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