The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Wed, 1 Oct 2003, Tyng-Ruey Chuang wrote:

> It seems to be that Coq toplevel understands type nat+nat+nat,
> which is different from nat+(nat+nat), but I cannot find Coq syntax
> to construct and desctruct values of this types.
>

nat+nat+nat is (nat+nat)+nat because of implicit left parenthesis.
It is indeed different from nat+(nat+nat).

You can then build a value in this type by using two levels of inl and inr:

(* left handside: *)
Coq < Check (inl nat+nat nat (inl nat nat O)).
(inl nat+nat nat (inl nat nat (0)))
     : nat+nat+nat

(* middle: *)
Coq < Check (inl nat+nat nat (inr nat nat O)).
(inl nat+nat nat (inr nat nat (0)))
     : nat+nat+nat

(* right handside *)
Coq < Check (inr nat+nat nat O).
(inl nat+nat nat (0))
     : nat+nat+nat


This ... + ... + ... syntax is similar to what is used in theorem
lt_eq_lt_dec (file Compare_dec.v):

Coq < Require Compare_dec.
Coq < Check lt_eq_lt_dec.
lt_eq_lt_dec
     : (n,m:nat){(lt n m)}+{n=m}+{(lt m n)}


Finally, if you really want a ternary "or" without this "two level"
encoding, you can do that via an new inductive definition:

Inductive ternary_or [A,B,C:Set] : Set :=
    the_left : A -> (ternary_or A B C)
  | the_middle : B -> (ternary_or A B C)
  | the_right : C -> (ternary_or A B C).


Pierre Letouzey