[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs-help@csl.sri.com*Subject*: where is possible to define recursive functions ?*From*: Michel Levy <Michel.Levy@imag.fr>*Date*: Fri, 12 Jul 2002 17:45:54 +0200*Sender*: pvs-help-owner@csl.sri.com

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 http://www-lsr.imag.fr/users/Michel.Levy/

- Prev by Date:
**associativity** - Next by Date:
**seeking proof of a trivial fact** - Prev by thread:
**Re: seeking proof of a trivial fact** - Next by thread:
**associativity** - Index(es):