Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Notation for partial terms

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Notation for partial terms


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.18.

Top of Page