The Coq mailing list

[Tyng-Ruey Chuang <trc AT iis.sinica.edu.tw>]

Ah, left associativity! Many thanks!

Tyng-Ruey

Pierre Letouzey wrote:

> 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
>
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>
>