Commit 268cf1fe authored by g.genestier's avatar g.genestier

Examples from BlanquiJouannaudRubio, CPO The End of A Quest

parent 851f7d80
#NAME ExamplesBJR.
(; The first nonterminaing example ;)
A : Type.
g : (A -> A) -> A.
def f : A -> A -> A.
[] f (g (x => f x x)) (g (x => f x x)) --> (x : A => f x x) (g (x : A => f x x)).
(; The Kop, van Raamsdong non terminating example ;)
O : Type.
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
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