Jakob Schulz (Dec 01 2022 at 14:37): Jakob Schulz (Dec 01 2022 at 14:37):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?
Manuel Eberl (Dec 01 2022 at 18:50):Works fine for me in Isabelle-2021-1. In what context are you running this?
Last updated: Apr 25 2024 at 08:20 UTC