[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
where is possible to define recursive functions ?
It's often the case that we need to define a recursive fonction locally
(in a let)
Example in Ocaml :
let reverse l =
let rec aux x y = match x with
| -> y
|a::u -> aux u (a::y)
in aux l ;;
A direct translation in PVS seems to me impossible, because I don't see
the possibility to use a recursive definition in a let binding.
Do you know if it's possible to have a local (inside a let) recursive
definition in PVS ?
36 rue George Sand 38400 Saint Martin d'Hères
email : Michel.Levy@imag.fr