Commit aa646139 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

A few updates of files

parent abe0baa9
......@@ -20,10 +20,12 @@ def concat : m : Nat -> Vect m -> n : Nat -> Vect n -> Vect (plus m n).
e : Elt.
(; Une définition légitimement refusée.
(; A définition refused as expected
def a := concat (S (S (S (S (S (S 0)))))) (Cons e 0 Nil) (S 0) (Cons 0 Nil).
;)
Tt : n : Nat -> Vect n -> Type.
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
(; 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 NonConfluenceTypeLevel.
N : Type.
0 : N.
S : N -> N.
def T : N -> N -> Type.
[x,y] T (S x) y --> N.
[x,y] T x (S y) --> N -> N.
......@@ -28,7 +28,7 @@ for line in toStudy:
toStudy.close()
toFill=open("../../Bureau/Resultats/data/"+sys.argv[1]+".csv",'w')
toFill.write(";;"+sys.argv[1]+";;,\n;;;;;\n")
toFill.write(";;"+sys.argv[1]+";;;\n;;;;;\n")
def printlist(couple):
if couple[1]==[]:
......
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