アルファ同値を確かめる例

by_elab seems to work fine. For instance:

def name1 : ℕ → (ℕ → ℕ) → ℕ := λ n f ↦ f n
def name2 : ℕ → (ℕ → ℕ) → ℕ := λ m g ↦ g m

def getDeclExpr (n : Name) : MetaM Expr := do
  let env ← getEnv
  match env.find? n with
  | some decl =>
    match decl.value? with
    | some val => return val
    | none     => throwError "Declaration {n} has no value (might be opaque or a constant)"
  | none => throwError "Declaration {n} not found"

#guard_expr (by_elab getDeclExpr `name1) =ₐ (by_elab getDeclExpr `name2)

The issue provides Lean definitions for name1 and name2, a getDeclExpr helper, and a #guard_expr alpha-equivalence check. Start by locating the repository's existing code examples and determine where this example belongs; done means the intended alpha-equivalence example is documented or added there and can be checked successfully.