Commit 9d358ccf authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

Wed 31 jan

parent ebdef507
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def f : Nat -> Nat -> Nat.
[x,y] f (S x) y --> f x (S x).
[x,y] f x (S y) --> f y x.
#NAME Expl.
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def minus : Nat -> Nat -> Nat.
[x] minus x 0 --> x.
[x,y] minus (S x) (S y) --> minus x y.
(; Caution, this division is the upper integer part which is not the usual one;)
def div : Nat -> Nat -> Nat.
[y] div 0 (S y) --> 0.
[x,y] div (S x) (S y) --> S (div (minus x y) (S y)).
......@@ -48,7 +48,9 @@ def f : R -> R -> R := plus (x : R => y : R => ch x) (x : R => y : R => sh y).
#SNF 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