coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Anders Lundstedt <anders AT anderslundstedt.se>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Notation for partial terms
- Date: Mon, 13 Jan 2014 08:40:29 +0100
Dear all,
given a partial binary operation
f : A -> A -> option A
is there a convenient way to write partial expressions (with left associativity)? I would like to be able to write e.g.
a*b*c*d
which would be equal to Some e if
a*b=Some x
x*c=Some y
y*d=Some e
for some x y : A, otherwise we would have a*b*c*d = None.
Best regards,
Anders Lundstedt
- [Coq-Club] Notation for partial terms, Anders Lundstedt, 01/13/2014
- Re: [Coq-Club] Notation for partial terms, Arnaud Spiwack, 01/13/2014
- Re: [Coq-Club] Notation for partial terms, Cedric Auger, 01/13/2014
- Re: [Coq-Club] Notation for partial terms, Anders Lundstedt, 01/13/2014
Archive powered by MHonArc 2.6.18.