Commit 400d0b70 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Merge branch 'master' of https://git.lsv.fr/genestier/PleinDeDk

parents beecfe4a 268cf1fe
#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