Khiem (Aug 31 2022 at 14:05): Khiem (Aug 31 2022 at 14:05):Hello,
I have really noobie question.
image.png
Why is the value line not outputting anything?
I just want to check my definition manually
Mathias Fleury (Aug 31 2022 at 14:08):you are missing quotes or cartouches after the expression after value
Khiem (Aug 31 2022 at 14:11):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: Oct 13 2024 at 01:36 UTC