Commit e798bd91 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Forme

parent 357cf141
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -7,3 +5,4 @@ S : Nat -> Nat.
def f : Nat -> Nat -> Nat.
[x,y] f (S x) y --> f x (S x).
[x,y] f x (S y) --> f y x.
#NAME Goodstein.
type : Type.
eps : type -> Type.
......@@ -111,5 +109,6 @@ def Goodstein_bis : Nat -> Nat -> Nat -> Nat.
[seed,remaining,base] Goodstein_bis seed (S remaining) base -->
Goodstein_bis (pred (raise base seed)) remaining (S base).
#SNF GoodsteinAll 3.
#SNF Goodstein 4 2.
\ No newline at end of file
#EVAL GoodsteinAll 3.
#EVAL Goodstein 4 2.
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -12,3 +10,4 @@ def minus : Nat -> Nat -> Nat.
def div : Nat -> Nat -> Nat.
[y] div 0 (S y) --> 0.
[x,y] div (S x) (S y) --> S (div (minus x y) (S y)).
......@@ -129,11 +129,19 @@ def moins : Nat -> Nat -> Nat.
[x] moins x 0 --> x.
[x,y] moins (S x) (S y) --> moins x y.
def Cbv : (Nat -> Nat) -> Nat -> Nat.
[f,x] Cbv f (S x) --> f (S x).
def McCarthy : Nat -> Nat.
def MC_aux : Nat -> Bool -> Nat.
[x] McCarthy x --> MC_aux x (leq x 100).
[x] McCarthy x --> Cbv (y => MC_aux y (leq y 100)) x.
[x] MC_aux x True --> McCarthy (McCarthy (plus x 11)).
[x] MC_aux x False --> moins x 10.
#EVAL McCarthy 81.
\ No newline at end of file
def McCarthy_opti : Nat -> Nat.
[x] McCarthy_opti (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) --> (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S x))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))).
[x] McCarthy_opti x --> McCarthy_opti (McCarthy_opti (plus x 11)).
#EVAL McCarthy 1.
#CHECK (McCarthy 1) == 91.
#NAME MillerPatternWithLambda.
A : Type.
f : A -> A -> A.
def g : (A -> A) -> A.
......@@ -16,5 +14,5 @@ a : A.
-->
a.
#CONV g (x => g (y => f x y)), a.
#CONV h (x => g (y => f x y)), a.
#CHECK g (x => g (y => f x y)) == a.
#CHECK h (x => g (y => f x y)) == a.
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -28,6 +26,6 @@ def eq : Nat -> Nat -> Nat.
def e := x : Nat => y : Nat => (eq x y).
#WHNF e.
#HNF e.
#SNF e.
\ No newline at end of file
#EVAL[WHNF] e.
#EVAL[HNF] e.
#EVAL[SNF] e.
......@@ -19,3 +19,4 @@ def 3 := S 2.
def 5 := S (S 3).
#EVAL[WHNF,1] f (plus 3 2) (mult 1 5).
......@@ -17,4 +17,5 @@ def b : A.
#EVAL[SNF] (f a b).
(; retourne g b ;)
#EVAL[WHNF] a.
(; retourne b ;)
\ No newline at end of file
(; retourne b ;)
#NAME Abstraction.
A : Type.
f: A -> A -> A.
def g: A -> (A -> A).
[x] g x --> (y : A => f y x).
#NAME AndPoly.
Bool : Type.
Nat : Type.
......@@ -46,4 +44,5 @@ def andb : n : Nat -> Bool_ n.
(; ;)
def g : n: Nat -> Bool_ n -> Bool.
[X] g (S (S (S 0))) X --> X True False True.
\ No newline at end of file
[X] g (S (S (S 0))) X --> X True False True.
#NAME append.
A : Type.
Nat: Type.
Z : Nat.
......@@ -17,3 +15,4 @@ def append: n : Nat -> Listn n -> m : Nat -> Listn m -> Listn (plus n m).
[l2] append _ nil _ l2 --> l2
[n,l1,m,l2,a]
append _ (cons n a l1) m l2 --> cons (plus n m) a (append n l1 m l2).
#NAME Associativity.
nat : Type.
0 : nat.
S : nat -> nat.
......@@ -21,4 +19,5 @@ def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
(; The linear version ;)
def concat : n : nat -> Vect n -> m : nat -> Vect m -> Vect (plus n m).
[n1,n2,n3,l1,l2,l3] concat _ (concat n1 l1 n2 l2) n3 l3 --> concat n1 l1 (plus n2 n3) (concat n2 l2 n3 l3).
(; ;)
\ No newline at end of file
(; ;)
#NAME BadlyTypedLhs.
N : Type.
0 : N.
......@@ -23,5 +21,6 @@ def eB : Bb -> Type.
(;
def phi : eB a -> Bb.
#CHECK a,eB a.
;)
\ No newline at end of file
#CHECK a : eB a.
;)
#NAME BTR.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -28,4 +26,5 @@ Tt : n : Nat -> Vect n -> Type.
(; Another one
b : Tt (S (S 0)) (concat (S (S (S (S (S (S 0)))))) (Cons e 0 Nil) (S 0) (Cons 0 Nil)).
;)
\ No newline at end of file
;)
#NAME bool.
Bool : Type.
def boucle : Bool -> Bool.
[x] boucle x --> boucle x.
#NAME cic.
Nat : Type.
z : Nat.
......
#NAME DeBruijn.
N : Type.
0 : N.
S : N -> N.
......@@ -37,19 +35,20 @@ def subst : N -> DB -> DB -> DB.
def delta := Lam (App (Var 0) (Var 0)).
#NSTEPS #2 beta (App delta delta).
#NSTEPS #19 beta (App delta delta).
#NSTEPS #36 beta (App delta delta).
#EVAL[2] beta (App delta delta).
#EVAL[19] beta (App delta delta).
#EVAL[36] beta (App delta delta).
def id := Lam (Var 0).
#SNF beta (App id id).
#SNF beta (App id delta).
#SNF beta (App delta id).
#EVAL[SNF] beta (App id id).
#EVAL[SNF] beta (App id delta).
#EVAL[SNF] beta (App delta id).
def left := Lam (Lam (Var (S 0))).
def right := Lam (Lam (Var 0)).
#SNF beta (App left id).
#SNF beta (App (App left id) (App delta delta)).
#SNF beta (Lam (App (Lam (Var (S 0))) id)).
\ No newline at end of file
#EVAL[SNF] beta (App left id).
#EVAL[SNF] beta (App (App left id) (App delta delta)).
#EVAL[SNF] beta (Lam (App (Lam (Var (S 0))) id)).
#NAME doubleCommut.
Nat : Type.
0 : Nat.
......@@ -10,4 +8,5 @@ def plus : Nat -> Nat -> Nat.
[m,n] plus (S m) n --> S (plus m n).
[x,y,z] plus x (plus y z) --> plus (plus x y) z.
[x,y,z] plus (plus x y) z --> plus x (plus y z).
\ No newline at end of file
[x,y,z] plus (plus x y) z --> plus x (plus y z).
#NAME Double.
Nat : Type.
0 : Nat.
......@@ -15,5 +13,6 @@ def double_ : Nat -> Nat := x => plus x x.
def f : (Nat -> Nat) -> Nat.
[] f (x=> plus x x) --> 0.
#SNF f double.
#SNF f double_.
\ No newline at end of file
#EVAL f double.
#EVAL f double_.
#NAME DownToZero.
Nat : Type.
0 : Nat.
......@@ -10,4 +8,5 @@ def down : Nat -> Nat.
[n] down (S n) --> down n.
def w : Nat.
[] w --> S w.
\ No newline at end of file
[] w --> S w.
#NAME ExamplesBJO.
type : Type.
arrow : type -> type -> type.
def eval : type -> Type.
......@@ -210,4 +208,5 @@ def intrecBis : A : type -> eval A -> (Int -> eval A -> eval A) -> (Int -> eval
[A, x, y, z, n] intrecBis A x y z (s_int n) --> y n (intrecBis A x y z n).
[A, x, y, z, n] intrecBis A x y z (p_int n) --> z n (intrecBis A x y z n).
def plus_int_rec : Int -> Int -> Int := x => y => intrec int x (x => y => s_int y) (x => y => p_int y) y.
\ No newline at end of file
def plus_int_rec : Int -> Int -> Int := x => y => intrec int x (x => y => s_int y) (x => y => p_int y) y.
#NAME ExamplesBJR.
(; The first nonterminaing example ;)
A : Type.
......@@ -14,4 +12,5 @@ def F : O -> O.
def b : O -> O -> O.
a : O.
[] b a a --> (z : O => F z) a.
[] F a --> b a a.
\ No newline at end of file
[] F a --> b a a.
#NAME bug.
nat : Type.
O : nat.
S : nat -> nat.
......@@ -21,4 +19,5 @@ def expandn : n : nat -> lnt n -> list -> lnt n.
a : t.
#SNF expandn O (List (S O) a) Nil.
#EVAL[SNF] expandn O (List (S O) a) Nil.
#NAME FO.
Term : Type.
Prop : Type.
def prf : Prop -> Type.
......@@ -90,3 +88,4 @@ def eq_sym: prf( forall (x:Term => forall (y:Term => (imp (equals x y) (equals y
def eq_trans: prf ( forall (x:Term => forall (y:Term => (forall (z:Term => imp (and (equals x y) (equals y z)) (equals x z))))) )
:= x:Term => y:Term => z:Term => p:prf (and (equals x y) (equals y z)) => P:(Term -> Prop) => q:prf (P x) =>
and_elim_2 (equals x y) (equals y z) p P (and_elim_1 (equals x y) (equals y z) p P q).
#NAME FOL.
Prop : Type.
prf : Prop -> Type.
......@@ -48,3 +46,4 @@ U:Type.
forall : (U->Prop) -> Prop.
forall_intro : P:(U->Prop) -> (x:U -> prf (P x)) -> prf (forall P).
forall_elim : P:(U->Prop) -> prf (forall P) -> x:U -> prf (P x).
#NAME fixpoint.
N : Type.
0 : N.
S : N -> N.
......@@ -35,5 +33,6 @@ def fac : (N -> N) -> (N -> N).
def ffact := fix2 fac.
#CONV ffact 5 , plus 100 (plus 10 10).
#CONV ffact 100, plus 100 (plus 10 10).
#CHECK ffact 5 == plus 100 (plus 10 10).
#CHECK ffact 100 == plus 100 (plus 10 10).
#NAME qualpat.
T : Type.
a : T.
......@@ -10,5 +8,6 @@ a : T.
will fail in this situation.
This test will be removed in the future. ;)
def f : T -> qualpat.T.
[] f qualpat.a --> a.
def f : T -> identifyingSameModule.T.
[] f identifyingSameModule.a --> a.
#NAME bug.
nat : Type.
O : nat.
S : nat -> nat.
......@@ -18,5 +16,6 @@ def id : n : nat -> lnt n -> lnt n.
[l] id _ l --> l.
(; Ici on obtient un Assertion Failed pour des problèmes d'arité
#SNF id O (g O).
(; ;)
\ No newline at end of file
#EVAL[SNF] id O (g O).
(; ;)
#NAME imperative.
type : Type.
def eps : type -> Type.
......@@ -136,7 +134,8 @@ def triple : (eps Nat) -> (eps Nat).
def while : A : type -> (eps A) -> ((eps A) -> (eps Bool)) -> ((eps A) -> (eps A)) -> (eps A).
[A,a,test,f] while A a test f --> if A (test a) (while A (f a) test f) a.
#SNF (while Nat 1 (x => leq x 100) triple).
#EVAL[SNF] (while Nat 1 (x => leq x 100) triple).
(;
#SNF (for Nat 1 1 10 double).
;)
\ No newline at end of file
#EVAL[SNF] (for Nat 1 1 10 double).
;)
#NAME IntBinaire.
Int : Type.
def Nat := Nat.Nat.
......@@ -48,4 +46,5 @@ def geq : Int -> Int -> Bool.
[x,y] geq (Neg x) (Pos y) --> F.
[x,y] geq (Neg x) (Neg y) --> Nat.geq y x.
#WHNF mult (Pos (Nat.x2 (Nat.x2plus1 Nat.1))) (Pos (Nat.x2 Nat.1)).
\ No newline at end of file
#EVAL[WHNF] mult (Pos (Nat.x2 (Nat.x2plus1 Nat.1))) (Pos (Nat.x2 Nat.1)).
#NAME lambdaCalcul.
lamt : Type.
Lam : (lamt -> lamt)-> lamt.
......@@ -9,4 +7,5 @@ def App : lamt -> lamt -> lamt.
def delta : lamt := Lam (x=> App x x).
#STEP ((x:lamt=> App x x) delta).
#EVAL[1] ((x:lamt=> App x x) delta).
#NAME LogiqueCombinatoire.
Lamt : Type.
Varia : Type.
......@@ -39,5 +37,5 @@ t : Lamt.
def B := Abst X1 (Abst X2 (App (Var X2) (App (App (Var X1) (Var X1)) (Var X2)))).
def Y := App B B.
#SNF (trad_lam2CL B).
#SNF (trad_lam2CL Y).
#EVAL (trad_lam2CL B).
#EVAL (trad_lam2CL Y).
......@@ -47,11 +47,11 @@ def flip : (R -> R -> R2) -> (R -> R -> R2).
def f : R -> R -> R := plus (x : R => y : R => ch x) (x : R => y : R => sh y).
#SNF flip (grad f).
#EVAL flip (grad f).
(;
#SNF #20 flip (grad f).
#EVAL #20 flip (grad f).
;)
#SNF grad (trans f).
#EVAL grad (trans f).
#CONV grad (trans f), flip (grad f).
#CHECK grad (trans f) == flip (grad f).
#NAME Monad.
type : Type.
eval : type -> Type.
M : type -> type.
......@@ -13,4 +11,5 @@ def bind : A : type -> B : type -> ((eval A) -> eval (M B)) -> eval (M A) -> eva
[A,B,C,e,k,l] bind C B l (bind A {C} k e) --> bind A B (x => bind C B l (k x)) e.
def comp : A : type -> B : type -> C : type -> ((eval A) -> eval (M B)) -> ((eval B) -> eval (M C)) -> (eval A) -> eval (M C)
:= A => B => C => f => g => a => bind B C g (f a).
\ No newline at end of file
:= A => B => C => f => g => a => bind B C g (f a).
#NAME multiarg.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
......@@ -8,4 +6,5 @@ def projec : Nat -> Nat -> Nat.
[x] projec x _ --> x.
def projecc : Nat -> Nat -> Nat -> Nat.
[x,y,z] projecc x y z --> projec x (projec y z).
\ No newline at end of file
[x,y,z] projecc x y z --> projec x (projec y z).
#NAME MutuallyDependant.
Tree : Type.
ListTree : Type.
node : ListTree -> Tree.
nil_tree : ListTree.
cons_tree : Tree -> ListTree -> ListTree.
#NAME Nat.
Nat : Type.
Bool : Type.
......@@ -68,4 +66,5 @@ def eq : Nat -> Nat -> Bool.
[x,y] eq (x2 x) (x2plus1 y) --> F.
[x] eq (x2plus1 x) 1 --> F.
[x,y] eq (x2plus1 x) (x2 y) --> F.
[x,y] eq (x2plus1 x) (x2plus1 y) --> eq x y.
\ No newline at end of file
[x,y] eq (x2plus1 x) (x2plus1 y) --> eq x y.
#NAME NatInductor.
type: Type.
nat : type.
......@@ -11,3 +9,4 @@ s : eps nat -> eps nat.
def natind: P: (eps nat -> type) -> eps (P 0) -> (n: eps nat -> eps (P n) -> eps (P (s n))) -> m: (eps nat) -> eps (P m).
[P,h0,hs] natind P h0 hs 0 --> h0.
[P,h0,hs,m] natind P h0 hs (s m) --> hs m (natind P h0 hs m).
#NAME nat_prop.
(;-------------------------------------------;)
(; Nat as first order terms ;)
(;-------------------------------------------;)
......@@ -149,6 +147,6 @@ def ack_is_pos : prf ack_is_pos_thm :=
(;
#WHNF fact_is_pos (exp 10 2).
#WHNF ack_is_pos 3 4.
#EVAL[WHNF] fact_is_pos (exp 10 2).
#EVAL[WHNF] ack_is_pos 3 4.
(;;)
#NAME NonConfluenceTypeLevel.
N : Type.
0 : N.
S : N -> N.
......@@ -7,3 +5,4 @@ S : N -> N.
def T : N -> N -> Type.
[x,y] T (S x) y --> N.
[x,y] T x (S y) --> N -> N.
#NAME essai.
A : Type.
B : Type.
C : ((A -> B) -> B) -> A.
def e : A -> B.
[f] e (C f) --> f e.
\ No newline at end of file
[f] e (C f) --> f e.
#NAME NumberBases.
Figure : Type.
0 : Figure.
1 : Figure.
......@@ -73,3 +71,4 @@ def hexadecimal_aux : Tuto.Nat -> Number -> Number.
[n,N] hexadecimal_aux (Tuto.S n) (Cons N D) --> hexadecimal_aux n (Cons N E).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N E) --> hexadecimal_aux n (Cons N F).
[n,N] hexadecimal_aux (Tuto.S n) (Cons N F) --> hexadecimal_aux n (Cons (hexadecimal_aux (Tuto.S Tuto.0) N) 0).
#NAME Produit.
type : Type.
eval : type -> Type.
......@@ -24,4 +22,5 @@ def Bool_ : n : eval Nat -> type.
def and_ : n : eval Nat -> eval (Bool_ n) -> eval Bool.
[] and_ 0 _ --> True.
[n,x] and_ (S n) (Pair _ _ True x) --> and_ n x.
[n] and_ (S n) (Pair _ _ False _) --> False.
\ No newline at end of file
[n] and_ (S n) (Pair _ _ False _) --> False.
#NAME lambdaCalculi.
def lamt : Type.
[] lamt --> lamt -> lamt.
def delta : lamt := (x => x x).
def omega : lamt := delta delta.
#HNF (x: lamt => (y: lamt => y)) omega.
\ No newline at end of file
#EVAL[HNF] (x: lamt => (y: lamt => y)) omega.
#NAME ReflexivityRoot.
nat : Type.
0 : nat.
S : nat -> nat.
......@@ -22,4 +20,5 @@ eq : nat -> nat -> Type.
refl : n : nat -> eq n n.
def root_correct (n : nat) : eq (root (mult n n) (sq n)) n
:= refl n.
\ No newline at end of file
:= refl n.
#NAME RuleOrder.
Nat : Type.
0 : Nat.
......@@ -27,17 +25,18 @@ def operation4 : Nat -> Nat -> Nat.
[x,y] operation4 (S x) y --> S 0.
[x,y] operation4 x (S y) --> S (S 0).
#SNF operation (S 0) (S 0).
#SNF operation2 (S 0) (S 0).
#SNF operation3 (operation3 (S 0) (S 0)) (S 0).
#SNF operation4 (operation4 (S 0) (S 0)) (S 0).
#EVAL[SNF] operation (S 0) (S 0).
#EVAL[SNF] operation2 (S 0) (S 0).
#EVAL[SNF] operation3 (operation3 (S 0) (S 0)) (S 0).
#EVAL[SNF] operation4 (operation4 (S 0) (S 0)) (S 0).
#EVAL[HNF] operation (S 0) (S 0).
#EVAL[HNF] operation2 (S 0) (S 0).
#EVAL[HNF] operation3 (operation3 (S 0) (S 0)) (S 0).
#EVAL[HNF] operation4 (operation4 (S 0) (S 0)) (S 0).
#HNF operation (S 0) (S 0).
#HNF operation2 (S 0) (S 0).
#HNF operation3 (operation3 (S 0) (S 0)) (S 0).
#HNF operation4 (operation4 (S 0) (S 0)) (S 0).
#EVAL[WHNF] operation (S 0) (S 0).
#EVAL[WHNF] operation2 (S 0) (S 0).
#EVAL[WHNF] operation3 (operation3 (S 0) (S 0)) (S 0).
#EVAL[WHNF] operation4 (operation4 (S 0) (S 0)) (S 0).
#WHNF operation (S 0) (S 0).
#WHNF operation2 (S 0) (S 0).
#WHNF operation3 (operation3 (S 0) (S 0)) (S 0).
#WHNF operation4 (operation4 (S 0) (S 0)) (S 0).
\ No newline at end of file
#NAME stlc.
type : Type.
o : type.
arrow : type -> type -> type.
......@@ -13,4 +11,4 @@ Lam : a : type -> b : type -> (term a -> term b) -> term (arrow a b).
c:term o.
#STEP App o o (Lam o o (x=> x)) c.
#EVAL[1] App o o (Lam o o (x=> x)) c.
#NAME sze.
o : Type.
c : o->o.
......@@ -8,4 +6,5 @@ def a : o.
[] a--> c a.
def f : o -> o.
[] f (c a)-->f a.
\ No newline at end of file
[] f (c a)-->f a.
#NAME Syracuse.
NatBin : Type.
1 : NatBin.
......@@ -37,5 +35,6 @@ def Syracuse : NatBin -> NatBin.
[x] Syracuse (x2plus1 x) --> Syracuse (plus 1 (mult 3 (x2plus1 x))).
(;
#SNF Syracuse (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2 (x2 (x2plus1 (x2 (x2 (x2 (x2 (x2plus1 (x2 (x2plus1 1))))))))))))))))).
(; ;)
\ No newline at end of file
#EVAL[SNF] Syracuse (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2plus1 (x2 (x2 (x2plus1 (x2 (x2 (x2 (x2 (x2plus1 (x2 (x2plus1 1))))))))))))))))).
(; ;)
#NAME TestSyntax.
o : Type.
def f : o -> o.
c : o.
......@@ -9,4 +7,5 @@ c : o.
[g: o->o] f (g c) --> c.
[g] f (x => g x c) --> c.
[g] f (x => g (f x) (f c)) --> c.
;)
\ No newline at end of file
;)
#NAME Tuto.
(; Les Types ;)
Nat : Type.
......@@ -265,4 +263,5 @@ def 0_right_neutral : n : Nat ->
[] 0_right_neutral 0 --> tt
[n] 0_right_neutral (S n) --> 0_right_neutral n.
#CONV factorielle 14, mult 95 95. (; Answer is of course NO ;)
\ No newline at end of file
#CHECK factorielle 14 == mult 95 95. (; Answer is of course NO ;)
#NAME TypeRewriting.
def A : Type.
B : Type.
def x : A.
y : B.
[] A --> B.
[] x --> y.
\ No newline at end of file
[] x --> y.
#NAME unaire.
Nat : Type.
Bool : Type.
......@@ -37,4 +35,5 @@ def Syracuse : Nat -> Bool.
[] Syracuse (S 0) --> True.
[n] Syracuse (S (S n)) --> Syracuse (ifThenElse (even n) (S (halfOf n)) (S (mult (S (S (S 0))) (S (S n))))).
#SNF Syracuse (S (S (S (S (S (S (S 0))))))).
\ No newline at end of file
#EVAL Syracuse (S (S (S (S (S (S (S 0))))))).
#NAME VectDependant.
Nat : Type.
0 : Nat.
......@@ -36,8 +34,8 @@ def 2 := S 1.
def 3 := S 2.
def suite := Cons 2 e (Cons 1 e (Cons 0 e Nil)).
#CHECK Tail_bis 2 (Cons_bis 3 e suite) , Vect 2.
#CHECK suite , Vect 3.
#CHECK Tail_bis 2 (Cons_bis 3 e suite) : Vect 2.
#CHECK suite : Vect 3.
(; Un double YES pour les CHECK, donc on ne veut pas pouvoir convertir l'un en l'autre ;)
def id_bis : n : Nat -> Vect (S_bis n) -> Vect (S_bis n).
......@@ -46,4 +44,4 @@ def id_bis : n : Nat -> Vect (S_bis n) -> Vect (S_bis n).
(; ;)
(; Sa version non-linéaire qui type-checke bien ;)
[n, x, l] id_bis n (Cons_bis n x l) --> (Cons_bis n x l).
(; ;)
\ No newline at end of file
(; ;)
#NAME vt.
Bool : Type.
Nat : Type.
......@@ -34,4 +32,5 @@ def aux : Nat -> Bool -> Nat.
;)
def reduceToZero : Nat -> Nat.
[] reduceToZero 0 --> 0
[x] reduceToZero (S x) --> reduceToZero x.
\ No newline at end of file
[x] reduceToZero (S x) --> reduceToZero x.
#NAME Wahlstedt.
Set : Type.
El : Set -> Type.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment