Commit 33b85eba authored by Guillaume GENESTIER's avatar Guillaume GENESTIER

New file, similar to OperationalSemantic.dk

parent 323146ea
Nat : Type.
0 : Nat.
S : Nat -> Nat.
def plus : Nat -> Nat -> Nat.
[y] plus 0 y --> y.
[x,y] plus (S x) y --> S (plus x y).
def mult : Nat -> Nat -> Nat.
[] mult 0 _ --> 0.
[x,y] mult (S x) y --> plus (mult x y) y.
def f : Nat -> Nat -> Nat.
[x] f x x --> x.
def 1 := S 0.
def 2 := S 1.
def 3 := S 2.
def 5 := S (S 3).
#EVAL[WHNF,1] f (plus 3 2) (mult 1 5).
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