関数のタクティクによる定義

def f1 : Nat → Nat → Nat := by exact (fun (n m: Nat) => n + m)
#check f1
def f2 (n: Nat): Nat → Nat := by 
  intro m
  exact n + m
#check f2
def f3 (n m: Nat): Nat := by 
  exact n + m
#check f3