The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2014/1/13 Anders Lundstedt <anders AT anderslundstedt.se>

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

Alternatively to A. Spiwack suggestion, you can also define:

Definition extension3 (x:option A) : A -> option A :=
  match x with
  | Some x' => f x'
  | _ => fun _ => None
  end
.

Notation "! a" := (Some a) (at level xx).
Notation "a * b" := (extension3 a b) (at level yy).
---
with xx < yy

Now, you would have to write "! a * b * c * d = ! e" (or "! a * b * c * d = Some e")
instead of "a * b * c * d = Some e" as you wished; still I do not think it is much annoying.

--
.../Sedrikov\...