DSL をエラボレータで評価する/ elab 使用例

Zulip: > How to evaluate a DSL using the elaborator?

open Lean hiding Expr
open Qq
elab "⟦" x:term "⟧" : term => do
  let e ← unsafe Elab.Term.evalTerm Expr q(Expr) x
  match eval_closed e with
  | .inr n => return q($n)
  | .inl x => throwError "{x} occurs"

open Expr
#check ⟦ plus (num 3) (num 5) ⟧ -- this is elaborated to 8
#check ⟦ plus (num 3) (var "x") ⟧ -- this reports an error: "x occurs"

Begin with the linked Zulip discussion and the provided elaborator snippet. Find the repository location for comparable Lean-by-example entries and check how examples are organized and rendered. Done means the DSL evaluation example is added in the project’s established format and demonstrates both the successful evaluation and the variable error shown.