函数、依值函数与函数类型的表达式🔗

用 λ 抽象定义函数🔗

假设我们想为一个函数定义表达式，该函数接受一个自然数 n 并返回 n + n。直接使用 Expr.lam 很容易在局部上下文、自由变量和德布鲁因索引的管理上出错。Lean 提供了更安全的辅助函数：先用 withLocalDeclD（或 withLocalDecl）引入局部变量，再用 mkLambdaFVars 构造 λ 抽象。下面是我们定义倍增函数表达式的方法：

open Lean Meta Elab

def doubleExpr : MetaM Expr :=
  withLocalDeclD `n (mkConst ``Nat) fun n => do
    let double ← mkAppM ``Add.add #[n, n]
    mkLambdaFVars #[n] double

函数 withLocalDeclD 有三个参数：局部变量的名字、它的类型（此处为 Nat），以及一个把新创建的局部变量作为参数的续延函数。在续延内部，我们可以用 mkAppM 把加法函数应用到 n 和 n 上，从而构建 λ 抽象的主体。最后，我们用 mkLambdaFVars 创建一个对局部变量 n 进行抽象的 λ 抽象。

为了说明如何使用这个表达式，我们可以写一个精译器（见精译），让我们能在项位置使用它：

elab "double%" : term =>
  doubleExpr

14#eval double% 7 -- 14

用 Π 类型定义依值函数🔗

我们可以用类似的技术为依值函数以及 ∀ 量化的命题定义表达式，它们在 Lean 中由 Π 类型表示。例如，我们可以按如下方式为命题 forall n : Nat, n = n 定义一个表达式：

def rflNatExpr : MetaM Expr :=
  withLocalDeclD `n (mkConst ``Nat) fun n => do
    let eqn ← mkEq n n
    mkForallFVars #[n] eqn

elab "rflnat%" : term => do
  rflNatExpr

example : rflnat% := by⊢ ∀ (n : Nat), n = n -- goal `∀ (n : Nat), n = n`
  simpAll goals completed! 🐙

例子：证明结论 `∀ (n : Nat), n = n`🔗

把上面两个构造放在一起，来证明结论 ∀ (n : Nat), n = n。我们将构造一个给出该结论证明的表达式，然后检查该表达式的类型确实是 ∀ (n : Nat), n = n。这会用到函数 inferType（推断表达式的类型）和 isDefEq（检查两个表达式是否在定义上相等）。

我们定义一个函数 rflNatExprProof，它构造结论 ∀ (n : Nat), n = n 的一个证明表达式，并检查其类型正确：

def rflNatExprProof : MetaM Bool := do
  let pf ← withLocalDeclD `n (mkConst ``Nat) fun n => do
    let pfN ← mkAppM ``Eq.refl #[n]
    mkLambdaFVars #[n] pfN
  let pfType ← inferType pf
  isDefEq pfType (← rflNatExpr)

true#eval rflNatExprProof -- true

用 `mkArrow` 定义函数类型🔗

对于非依值的函数类型，我们可以用 mkArrow 函数来构建函数类型的表达式。例如，我们可以按如下方式为从 Nat 到 Nat 的函数类型定义一个表达式：

def natToNatExpr : MetaM Expr :=
  mkArrow (mkConst ``Nat) (mkConst ``Nat)

函数、依值函数与函数类型的表达式🔗

用 λ 抽象定义函数🔗

用 Π 类型定义依值函数🔗

例子：证明结论 ∀ (n : Nat), n = n🔗

用 mkArrow 定义函数类型🔗

例子：证明结论 `∀ (n : Nat), n = n`🔗

用 `mkArrow` 定义函数类型🔗