Hello!
I am playing around with WhyML and I noticed that I am unable to use a
`let rec` function with `map`. Below is a small code example that causes
the error "File xyz.ml, line 15, characters 2-153: Ident DECR eval is
not yet declared" to appear.
Is there something I'm missing on how to use higher order functions or
is this a limitation in WhyML/Why3 (I'm using version 1.3.1) at the moment?
Best regards,
Thomas
-----------------
module Test
use list.List
type expr = Const int
| Sum (list expr)
let rec function map (f: 'a -> 'b) (l: list 'a) : list 'b
variant { l }
= match l with
| Nil -> Nil
| Cons x xs -> Cons (f x) (map f xs)
end
let rec eval (e: expr) : int
variant { e }
= match e with
| Const i -> i
| Sum args ->
let args' = map eval args in
0
end
end
_______________________________________________
Why3-club mailing list
[email protected]
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
