Commit be0b67aa authored by g.genestier's avatar g.genestier

A new file, experimenting conv bug

parent beaa8b82
......@@ -9,6 +9,7 @@ verine/*
zenon_dk/*
focalide_dks/*
holide_lib/*
iProverModulo_dk/*
iProverModulo/*
dklib-master/*
TermChecker/*.txt
......
#NAME test.
N : Type.
0 : N.
B : Type.
T : B.
def A : B -> Type.
def f : A T -> Type.
[] f B --> B.
def Aa : Type.
def eA : Aa -> Type.
a : Aa.
[] Aa --> eA a.
Bb : Type.
def eB : Bb -> Type.
[] eB a --> eA a.
def phi : eB a -> Bb.
#CHECK a,eB a.
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