elab 使用例：termElab を使って無名コンストラクタ風の記法を定義する

import Lean

section
/- # 無名コンストラクタ風の記法を実装する
metaprogramming book より引用
-/

open Lean Elab Term Meta Term Command

/-- `typ` のコンストラクタをリストとして取得する。 -/
def getCtors (typ : Name) : TermElabM (List Name) := do
  -- 環境を取得する
  let env ← getEnv
  match env.find? typ with
  | some (ConstantInfo.inductInfo val) =>
    -- typ が帰納型の場合は、コンストラクタを取得する
    pure val.ctors
  | _ => pure []

/- `TermElab` の項は `CommandElab` の項とは異なり、引数の数が2つある関数になっている -/
example : CommandElab = (Syntax → CommandElabM Unit) := rfl
example : TermElab = (Syntax → Option Expr → TermElabM Expr) := rfl

/-- 無名コンストラクタ風の記法。

`<= typ` の部分が、`TermElab` の `Expr` 型の引数を表している。これは期待される型を表す。
これは糖衣構文であり、情報が十分にない場合に一度待つプロセス（postpone）を省略できる。
-/
elab "⟨⟨" args:term,* "⟩⟩" : term <= typ => do
  -- typ がメタ変数というのは typ が分からないことを表す。
  -- 期待されている型がわからなければしょうがないのでエラーにする
  if typ.isMVar then
    throwError "expected type must be known"

  -- `typ` が `type = f a₁ ... aₙ` の形であることを確認して
  -- `f` を取得し、`base` に格納する
  let Expr.const base .. := typ.getAppFn | throwError s!"type is not of the expected form: {typ}"

  -- `base` のコンストラクタを取得する
  let [ctor] ← getCtors base | throwError "type doesn't have exactly one constructor"

  -- `args` をコンストラクタに適用した式を作成する
  let stx ← `($(mkIdent ctor) $args*)

  elabTerm stx typ

#check (⟨⟨1, by omega⟩⟩ : Fin 12)
#check_failure ⟨⟨1, by omega⟩⟩ -- expected type must be known
#check_failure (⟨⟨0⟩⟩ : Nat) -- type doesn't have exactly one constructor
#check_failure (⟨⟨⟩⟩ : Nat → Nat) -- type is not of the expected form: Nat -> Nat

-- Lean の組み込みの無名コンストラクタとは異なり、
-- ネストされた帰納型を扱うことができない
#check_failure (⟨⟨ trivial, trivial, trivial ⟩⟩ : True ∧ True ∧ True)
#check (⟨trivial, trivial, trivial⟩ : True ∧ True ∧ True)

-- Lean の組み込みの無名コンストラクタとは異なり、
-- 定義を展開しない

abbrev FinPrime := Fin

#check_failure (⟨⟨1, by omega⟩⟩ : FinPrime 12) -- { val := 1, isLt := (_ : 1 < 12) } : Fin 12
#check (⟨1, by omega⟩ : FinPrime 12)

end

Start by reading the issue's standalone termElab example, especially getCtors and the anonymous-constructor elaborator. The payload does not name a target file, test, or specific documentation change, so the intended placement and completion criteria need to be established before work begins.