Re: [isabelle] Failed to parse term



Hi,

> primrec rotate1 :: "'a list => 'a list" where
> "rotate1 [] = []" |
> "rotate1 (x # xs) = xs @ [x]"
> value "rotate1 (1 # 2 # 3 # 4 # [])"

What is the purpose of this function? I cannot figure this out from your code.

> value "mmap +1 (1 # 2 # [])"
> failed to parse term

I guess you want to create a function by "+1" but Isabelle does not understand this syntax.

value "map (λt. t + 1) [0,1,2]"

is the correct way to express that. The presence of space after the dot is significant.

- Gergely


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.