[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 ?

	Sincerely yours 
Michel Levy
36 rue George Sand 38400 Saint Martin d'Hères
email : Michel.Levy@imag.fr