Stream: Beginner Questions

Topic: Running simple code


view this post on Zulip 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

view this post on Zulip Mathias Fleury (Aug 31 2022 at 14:08):

you are missing quotes or cartouches after the expression after value

view this post on Zulip 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"

view this post on Zulip Mathias Fleury (Aug 31 2022 at 14:14):

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"

view this post on Zulip Khiem (Aug 31 2022 at 14:21):

Ahh I got it. I had some errors with the theory name and file names


Last updated: Feb 27 2024 at 08:17 UTC