Commit 40a883f6 authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

A new file

parent 7a7e9585
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[x] plus x 0 --> x.
[x,y] plus x (S y) --> S (plus x y).
def double : Nat -> Nat.
[x] double x --> plus x x.
def f : Nat -> Nat -> Nat.
[x,y] f (double x) y --> S (S (S (S (S 0)))).
[x,y,z] f (plus x y) z --> S (S (S (S 0))).
[x,y] f (S (S x)) 0 --> 0.
[x,y] f x (S y) --> S 0.
[x,y] f (S (S x)) (S y) --> S (S (S 0)).
#SNF (f (double 0) 0).
#SNF (f (S (S 0)) (S (S 0))).
def eq : Nat -> Nat -> Nat.
[x] eq x x --> S 0.
[x,y] eq x y --> 0.
def e := x : Nat => y : Nat => (eq x y).
#WHNF e.
#HNF e.
#SNF e.
\ No newline at end of file
......@@ -48,7 +48,7 @@ def f : R -> R -> R := plus (x : R => y : R => ch x) (x : R => y : R => sh y).
#SNF flip (grad f).
#NSTEPS #20 flip (grad f).
#SNF #20 flip (grad f).
#SNF grad (trans f).
......
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