10 lines
184 B
Text
10 lines
184 B
Text
def f (x y : Nat) : Nat :=
|
|
x + 2*y
|
|
|
|
-- "+" with priority higher than the builtin "+" notation
|
|
infix:65 [high] "+" => f
|
|
|
|
#check 1 + 2
|
|
|
|
theorem ex (x y : Nat) : x + y = f x y :=
|
|
rfl
|