Commit b4755d77 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Readability

parent 79663c59
#NAME BadlyTypedLhs. #NAME BadlyTypedLhs.
N : Type. N : Type.
0 : N. 0 : N.
B : Type. B : Type.
T : B. T : B.
def A : B -> Type. def A : B -> Type.
def f : A T -> Type. def f : A T -> Type.
[] f B --> B. [] f B --> B.
def Aa : Type. def Aa : Type.
def eA : Aa -> Type. def eA : Aa -> Type.
a : Aa. a : Aa.
...@@ -22,7 +18,6 @@ a : Aa. ...@@ -22,7 +18,6 @@ a : Aa.
Bb : Type. Bb : Type.
def eB : Bb -> Type. def eB : Bb -> Type.
[] eB a --> eA a. [] eB a --> eA 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