Commit e0eb6d17 authored by Gaspard Ferey's avatar Gaspard Ferey

merge

parents 4d34df61 d8eafa8d
#NAME bug.
type : Type.
def term : type -> Type.
arr : type -> type -> type.
[A,B] term (arr A B) --> term A -> term B.
E : A : type -> term A -> type.
r : A : type -> a : term A -> term (E A a).
A : type.
B : type.
def e : f : (term A -> term B) ->
(x : term A -> term (E B (f x))) ->
term (E (arr A B) f).
[f] e f (x => r B (f x)) --> r (arr A B) f.
f : term (arr A B).
#EVAL e f (x : term A => r B (f x)).
#EVAL e (x => f x) (x : term A => r B (f x)).
#ASSERT (f : term (arr A B) => e (x => f x) (x : term A => r B (f x))) ==
(f : term (arr A B) => r (arr A B) f).
\ No newline at end of file
nat : Type.
0 : nat.
S : nat -> nat.
def A : (nat -> nat) -> (nat -> nat) -> nat -> nat.
[f] A f (x => f x) --> f.
#EVAL A (x : nat => 0) (x : nat => 0).
#CHECK A (x : nat => 0) (x : nat => 0) : nat -> nat.
\ No newline at end of file
N : Type.
0 : N.
S : N -> N.
def a : N -> N.
def b : N -> N.
def c : N -> N.
[x] a (S x) --> b (S x).
[x] b (S x) --> c (S x).
[x] c (S x) --> a x.
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