I have really noobie question.
Why is the value line not outputting anything?
I just want to check my definition manually
you are missing quotes or cartouches after the expression after value
Hey. It does not work. Even with the Quotes.
theory Untitled-1 imports Main begin fun count :: "'a list ⇒ 'a ⇒ nat" where "count  _ = 0" | "count (x#xs) x' = (if x = x' then Suc (count xs x') else count xs x')" value "count [1,2,3,4] 4"
ah yes, value does not know anything about the type "'a" (maybe all values are equal?). For experiments, I recommand using nat:
value "count [1::nat,2,3,4] 4"
Ahh I got it. I had some errors with the theory name and file names
Last updated: Dec 07 2023 at 20:16 UTC