Hi all :) I'm currently having trouble to understand the behaviour of the value
-command when working with functions that return pairs.
The minimal working example that I found was the following: when I try
fun test where "test a = a"
value "test (0::nat, 0::nat)"
then the value
-command says "No code equations for test". However,
value "id (0::nat, 0::nat)"
works and produces the desired result. What is happening here?
Works fine for me in Isabelle-2021-1. In what context are you running this?
Last updated: Jan 05 2025 at 16:21 UTC