MyLogicType.v

  Inductive ORT [A,B:Type]: Type :=
     LeftT: A->(ORT A B)
   | RightT: B->(ORT A B).

Section TListes.

  Variable A: Type.

  Inductive TList: Type :=
      TNl: TList
    | TCs: A->TList->TList.

  Fixpoint Tnth_def [d:A; l:TList]: nat->A :=
    [n:nat]Cases l n of
         TNl _ => d
       | (TCs x _) O => x
       | (TCs _ tl) (S k) => (Tnth_def d tl k)
       end.

  Inductive TIns [x:A]: nat->TList->TList->Prop :=
      TIns_hd: (l:TList)(TIns x O l (TCs x l))
    | TIns_tl: (n:nat)(l,il:TList)(y:A)(TIns x n l il)
                    ->(TIns x (S n) (TCs y l) (TCs y il)).

  Inductive TTrunc: nat->TList->TList->Prop :=
     Ttr_O: (e:TList)(TTrunc O e e)
   | Ttr_S: (k:nat)(e,f:TList)(x:A)(TTrunc k e f)
                                      ->(TTrunc (S k) (TCs x e) f).

  Hint Ttr_O Ttr_S.

End TListes.

  Hint TIns_hd TIns_tl Ttr_O Ttr_S.

06/11/96, 12:32