coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: Monad (Re: [Coq-Club] Unification)

From: Thery Laurent <thery AT ns.di.univaq.it>
To: David Nowak <David.Nowak AT lsv.ens-cachan.fr>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: Monad (Re: [Coq-Club] Unification)
Date: Thu, 3 Feb 2005 15:45:26 +0100 (CET)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

What about using exception monad? Could you then extract an exact call-by-value translation of the algorithm?

Yes I could have used monad (I've used a simple option type instead) but to my knowledge,the extraction would never give you back a code that uses directly the exception mechanism of ocaml.

--
Laurent

[Coq-Club] Unification, Colin Riba
- Re: [Coq-Club] Unification, Claude Marche
  - Re: [Coq-Club] Unification, Thery Laurent
    - Monad (Re: [Coq-Club] Unification), David Nowak
      - Re: Monad (Re: [Coq-Club] Unification), Jean-Christophe Filliatre
      - Re: Monad (Re: [Coq-Club] Unification), Thery Laurent
        
        Re: Monad (Re: [Coq-Club] Unification), David Nowak
- Re: [Coq-Club] Unification, Conor McBride