5. Embedded Domain-Specific Language

「今有物，不知其數。三三數之，賸二；五五數之，賸三；七七數之，賸二。問：物幾何？答曰：二十三。

術曰：三三數之，賸二，置一百四十；五五數之，賸三，置六十三；七七數之，賸二，置三十。并之，得二百三十三，以二百一十減之，即得。凡三三數之，賸一，則置七十；五五數之，賸一，則置二十一；七七數之，賸一，則置十五。一百六以上，以一百五減之，即得。」
《孫子算經》

Two promises remain, and this chapter keeps the first: the object language becomes resident in Lean, its programs written directly in Lean files, parsed by Lean, spliced into Lean definitions, and run, with no external pipeline left. The second promise, that something be proved about the language, is chapter 6's, and residence is what makes it convenient to keep.

The grammar, declared

Chapter 1 built the surface grammar out of combinators, one design decision at a time. Here is the same grammar again, as a syntax category:

declare_syntax_cat dtt

syntax:max (name := dttIdent) ident : dtt
syntax:max "U" : dtt
syntax:max "Unit" : dtt
syntax:max "unit" : dtt
syntax:max "(" dtt ")" : dtt
syntax:65 dtt:65 ppSpace dtt:66 : dtt
syntax:25 dtt:26 " -> " dtt:25 : dtt
syntax:25 "(" ident " : " dtt ")" " -> " dtt:25 : dtt
syntax:10 "fun " ident "." ppSpace dtt:10 : dtt
syntax:10 "fun " "(" ident " : " dtt ")" ". " dtt:10 : dtt
syntax:10 "let " ident " : " dtt " = " dtt "; " dtt:10 : dtt

The declarations carry the precedence table in their level annotations: application at 65 binding tighter than arrows at 25, binders lowest at 10, atoms at the maximum. The numbers are ordinals, not magnitudes; all that matters is their order, and the gaps are headroom for productions added later. Associativity hides in the off-by-ones: the arrow parses its left operand at 26 while sitting at 25 itself, so a second arrow can only continue on the right, which is right associativity, and application parses its right operand at 66, one above itself, so a chain can only grow leftward. Chapter 1 encoded the same two facts as a right-recursive descent and a left fold. The left-factor that chapter 1 spent a section on, the two productions beginning with (, is nowhere to be seen: Lean's parser tries same-token alternatives with backtracking and keeps the longest match, silently performing what attempt had to request. One token did not survive the move, and the swap is instructive. A backslash would clear the tokenizer without complaint, and the printer on this very page still emits one, in the backslash lambdas the demonstrations below display. What it collides with is the abbreviation convention every Lean editor builds in, where a leading backslash begins a Unicode abbreviation rather than a term. The resident lambda is therefore spelled fun, borrowing the host's own binder keyword, and the rent is paid to the host's conventions rather than to its lexer.

Down to Raw, again

The bridge back to the rest of the lectures is one function: syntax patterns destruct each production into chapter 1's Raw, and everything downstream, the checker of chapter 2, the backend of chapter 4, works unchanged. The same strings, one keyword aside; two parsers, one tree.

/-- Lean's `ident` lexes more than the object language means by a name: a
dotted path like `a.x` arrives as one identifier token. Names here are
single words, so anything else is refused rather than truncated. -/
def simpleName (x : Ident) : Except String String :=
  match x.getId.eraseMacroScopes with
  | .str .anonymous s => pure s
  | n => throw s!"object-language names are single words; {n} is not"

partial def rawOfSyntax (stx : TSyntax `dtt) : Except String Raw :=
  match stx with
  | `(dtt| $x:ident) => do pure (.var (<- simpleName x))
  | `(dtt| U) => pure .univ
  | `(dtt| Unit) => pure .unitType
  | `(dtt| unit) => pure .unitElem
  | `(dtt| ($t)) => rawOfSyntax t
  | `(dtt| $fn $arg) => do
    pure (.app (<- rawOfSyntax fn) (<- rawOfSyntax arg))
  | `(dtt| $dom -> $cod) => do
    pure (.pi "_" (<- rawOfSyntax dom) (<- rawOfSyntax cod))
  | `(dtt| ($x:ident : $dom) -> $cod) => do
    pure (.pi (<- simpleName x) (<- rawOfSyntax dom) (<- rawOfSyntax cod))
  | `(dtt| fun $x. $body) => do
    pure (.lam (<- simpleName x) none (<- rawOfSyntax body))
  | `(dtt| fun ($x:ident : $dom). $body) => do
    pure (.lam (<- simpleName x) (some (<- rawOfSyntax dom))
      (<- rawOfSyntax body))
  | `(dtt| let $x : $ty = $val; $body) => do
    pure (.letE (<- simpleName x) (<- rawOfSyntax ty) (<- rawOfSyntax val)
      (<- rawOfSyntax body))
  | _ => throw "unsupported syntax"

The issue promised in chapter 3 appears here: identifiers arriving through quotations carry hygiene marks, and eraseMacroScopes strips them so the object language sees the name the user wrote. A quieter mismatch is settled here too. Lean's ident means more than this language does by a name: a dotted path like a.x arrives as one identifier token, naming a namespace the object language does not have. The helper simpleName accepts exactly the single-word names and refuses the rest, rather than quietly truncating them to their last component; the commands below show the refusal, pinned like every other error.

Two parsers, rule by rule

Placing the two parsers side by side, production by production, shows what the declarations buy. On the left, chapter 1's combinators: every design decision, the commit points, the explicit attempt, the left fold that builds application spines, is spelled out in code. On the right, the same production as one declaration, the decisions compressed into precedence numbers. The comparison echoes the one chapter 2 drew between undirected typing rules and their moded versions: a grammar on paper is a relation between strings and trees, not an algorithm. By hand, chapter 1 turned that relation into one, choosing where to commit and where to backtrack; the syntax command performs the same turn mechanically, and the two algorithms disagree only where the chapter's opening said, at the token for lambda.

And the comparison need not stay on paper. A small helper runs both parsers on the same program, chapter 1's on a string and Lean's on the quoted syntax, and demands the same Raw tree, so each row below closes with parses that really execute, pinned by the build:

/-- Run both parsers on the same program, chapter 1's on the string and
Lean's on the quoted syntax, and demand the same `Raw` tree. -/
def parsersAgree (s : String) (stx : Unhygienic (TSyntax `dtt)) : Bool :=
  match parseRaw s, rawOfSyntax (Unhygienic.run stx) with
  | some fromCombinators, .ok fromSyntax => fromCombinators == fromSyntax
  | _, _ => false

The atoms: keywords, variables, and the parenthesis:

partial def pAtom : Parser Raw :=
  (do
    sym "("
    let t <- pTerm
    sym ")"
    pure t)
  <|> (do keyword "U"; pure .univ)
  <|> (do keyword "Unit"; pure .unitType)
  <|> (do keyword "unit"; pure .unitElem)
  <|> (do let x <- ident; pure (.var x))

syntax:max (name := dttIdent) ident : dtt
syntax:max "U" : dtt
syntax:max "Unit" : dtt
syntax:max "unit" : dtt
syntax:max "(" dtt ")" : dtt

#guard parsersAgree "U" `(dtt| U)
#guard parsersAgree "Unit" `(dtt| Unit)
#guard parsersAgree "unit" `(dtt| unit)
#guard parsersAgree "(x)" `(dtt| (x))

Application, a left-growing spine:

partial def pSpine : Parser Raw := do
  let fn <- pAtom
  let args <- many pAtom
  pure (args.foldl .app fn)

syntax:65 dtt:65 ppSpace dtt:66 : dtt

#guard parsersAgree "f x y" `(dtt| f x y)
#guard parsersAgree "f (g x)" `(dtt| f (g x))

Arrows and the dependent binder, with the left-factor on one side and longest-match backtracking on the other:

/-- The left-factor: commit to a dependent binder only after `( ident :`. -/
partial def pBinder : Parser (String × Raw) := do
  let x <- attempt (do
    sym "("
    let x <- ident
    sym ":"
    pure x)
  let dom <- pTerm
  sym ")"
  pure (x, dom)

partial def pArrows : Parser Raw :=
  (do
    let (x, dom) <- pBinder
    sym "->"
    let cod <- pArrows
    pure (.pi x dom cod))
  <|> (do
    let dom <- pSpine
    (do
      sym "->"
      let cod <- pArrows
      pure (.pi "_" dom cod))
    <|> pure dom)

syntax:25 dtt:26 " -> " dtt:25 : dtt
syntax:25 "(" ident " : " dtt ")" " -> " dtt:25 : dtt

#guard parsersAgree "A -> B -> C" `(dtt| A -> B -> C)
#guard parsersAgree "(A : U) -> A -> A" `(dtt| (A : U) -> A -> A)

The lambda, annotated and bare:

partial def pLam : Parser Raw := do
  sym "\\"
  (do
    let (x, dom) <- pBinder
    sym "."
    let body <- pTerm
    pure (.lam x (some dom) body))
  <|> (do
    let x <- ident
    sym "."
    let body <- pTerm
    pure (.lam x none body))

syntax:10 "fun " ident "." ppSpace dtt:10 : dtt
syntax:10 "fun " "(" ident " : " dtt ")" ". " dtt:10 : dtt

#guard parsersAgree "\\x. x" `(dtt| fun x. x)
#guard parsersAgree "\\(x : Unit). x" `(dtt| fun (x : Unit). x)

And let, one keyword and three separators on both sides:

partial def pLet : Parser Raw := do
  keyword "let"
  let x <- ident
  sym ":"
  let ty <- pTerm
  sym "="
  let val <- pTerm
  sym ";"
  let body <- pTerm
  pure (.letE x ty val body)

syntax:10 "let " ident " : " dtt " = " dtt "; " dtt:10 : dtt

#guard parsersAgree "let u : Unit = unit; u" `(dtt| let u : Unit = unit; u)

One asymmetry has no right-hand counterpart at all: chapter 1's pTerm dispatches between lambda, let, and arrows by trying them in order, and no declaration answers it, because ordering alternatives is exactly what the precedence levels already do. The identifier row hides the opposite asymmetry: the borrowed ident accepts dotted names that chapter 1's one-word identifiers never could, which is why the bridge back to Raw refuses them.

Judgments with contexts

The commands can grow declaration contexts now that the grammar is Lean's: a telescope of typed names before the turnstile, each inheriting the universe and bound in order. The two commands share their whole front half, one helper that binds the context and synthesizes the term; each command is then its single reporting line, and the difference between checking and evaluating is exactly that line. The names flip with the parser, and the flip is deliberate, because both generations survive in the build: #check_dtt and #eval_dtt are chapter 2's commands, a quoted string handed to chapter 1's parser, while #dtt_check and #dtt_eval take the program itself, parsed by Lean from the same file that states the judgment. The quotes are gone, and with them the escaped backslashes.

syntax dttDecl := "(" ident " : " dtt ")"

open Elab Command in
/-- The front half both judgment commands share: bind each declaration
into the context, then expand, translate, and synthesize the term. -/
def elabJudgment (decls : TSyntaxArray ``dttDecl) (t : TSyntax `dtt) :
    CommandElabM (Cxt × Tm × Val) := do
  let mut cxt := Cxt.empty
  for decl in decls do
    let `(dttDecl| ($x : $ty)) := decl
      | throwError "malformed declaration"
    let name <- ofExcept (simpleName x)
    let ty : TSyntax `dtt := ⟨<- liftMacroM (expandMacros ty)⟩
    let tyRaw <- ofExcept (rawOfSyntax ty)
    match inherit cxt tyRaw .univ with
    | .error e => throwError e
    | .ok ty' =>
      cxt := cxt.bind name (eval cxt.env ty')
  let t : TSyntax `dtt := ⟨<- liftMacroM (expandMacros t)⟩
  let raw <- ofExcept (rawOfSyntax t)
  match synth cxt raw with
  | .error e => throwError e
  | .ok (tm, ty) => return (cxt, tm, ty)

open Elab Command in
elab "#dtt_check " decls:dttDecl* " |- " t:dtt : command => do
  let (cxt, tm, ty) <- elabJudgment decls t
  logInfo s!"{showTm cxt tm} : {showTy cxt ty}"

open Elab Command in
elab "#dtt_eval " decls:dttDecl* " |- " t:dtt : command => do
  let (cxt, tm, ty) <- elabJudgment decls t
  logInfo s!"{showTm cxt (quote cxt.lvl ty (eval cxt.env tm))} : {showTy cxt ty}"

/-- info: \(x : A). x : (x : A) -> A -/
#guard_msgs in
#dtt_check (A : U) |- fun (x : A). x

/-- info: x : A -/
#guard_msgs in
#dtt_check (A : U) (x : A) |- x

/-- error: unknown variable y -/
#guard_msgs in
#dtt_check (A : U) (x : A) |- y

/-- error: object-language names are single words; a.x is not -/
#guard_msgs in
#dtt_check |- a.x

Longer programs ride the same turnstile. A chain of definitions reads like a file in the object language, and the two commands answer two different questions about it: #dtt_check echoes the elaborated program with its type, and #dtt_eval normalizes it away:

/--
info: let id : (A : U) -> A -> A = \A. \x. x; let twice : (A : U) -> (A -> A) -> A -> A = \A. \f. \x. f (f x); twice Unit (id Unit) unit : Unit
-/
#guard_msgs in
#dtt_check |-
  let id : (A : U) -> A -> A = fun A. fun x. x;
  let twice : (A : U) -> (A -> A) -> A -> A = fun A. fun f. fun x. f (f x);
  twice Unit (id Unit) unit

/-- info: unit : Unit -/
#guard_msgs in
#dtt_eval |-
  let id : (A : U) -> A -> A = fun A. fun x. x;
  let twice : (A : U) -> (A -> A) -> A -> A = fun A. fun f. fun x. f (f x);
  twice Unit (id Unit) unit

/-- info: \x. unit : (x : Unit) -> Unit -/
#guard_msgs in
#dtt_eval (f : Unit -> Unit) |- fun (x : Unit). f x

Arithmetic without numbers

The language has no numbers, yet it can count. A Church numeral is a function that iterates: given a type, a step, and a start, the numeral n applies the step n times. The type of numerals quantifies over the universe and lands back in it, which is the U : U shortcut of chapter 2 earning its keep; a stratified theory would need a universe level here. Addition iterates the successor, and the answer is computed by nothing but normalization, the evaluator of chapter 2 running under three binders:

/-- info: \A. \f. \x. f (f (f (f (f x)))) : (A : U) -> (f : A -> A) -> (x : A) -> A -/
#guard_msgs in
#dtt_eval |-
  let N : U = (A : U) -> (f : A -> A) -> (x : A) -> A;
  let two : N = fun A. fun f. fun x. f (f x);
  let three : N = fun A. fun f. fun x. f (f (f x));
  let add : N -> N -> N = fun m. fun n. fun A. fun f. fun x. m A f (n A f x);
  add two three

/--
info: \A. \f. \x. f (f (f (f (f (f (f x)))))) : (A : U) -> (f : A -> A) -> (x : A) -> A
-/
#guard_msgs in
#dtt_eval |-
  let N : U = (A : U) -> (f : A -> A) -> (x : A) -> A;
  let two : N = fun A. fun f. fun x. f (f x);
  let three : N = fun A. fun f. fun x. f (f (f x));
  let add : N -> N -> N = fun m. fun n. fun A. fun f. fun x. m A f (n A f x);
  two N (add two) three

The second command deserves a second look: the numeral two is instantiated at the type of numerals itself, so its step function is "add two" and its start is three, computing $3 + 2 + 2$ . Numerals consuming numerals is the impredicativity of U : U made tangible, and the normal forms the build pins are the whole proof that the machinery works.

The splice

Residence is completed by one elaborator, and its name declares its ancestry: as by embeds the tactic language in term position, by_dtt embeds the object language, the program compiled through chapter 4's backend into the Expr Lean was about to elaborate anyway. An object program is now an ordinary Lean value; #guard runs it, and a spliced function applies to Lean arguments.

open Elab Term in
elab "by_dtt " t:dtt : term => do
  let t : TSyntax `dtt := ⟨<- liftMacroM (expandMacros t)⟩
  let raw <- ofExcept (rawOfSyntax t)
  match synth Cxt.empty raw with
  | .error e => throwError "our checker refuses: {e}"
  | .ok (tm, _) =>
    match compile tm with
    | .error e => throwError e
    | .ok e => pure e

#guard (by_dtt (fun (x : Unit). x) unit) == ()

def applyTwice :=
  by_dtt fun (f : Unit -> Unit). fun (x : Unit). f (f x)

#guard applyTwice (fun u => u) () == ()

Like by, the form is open at the right, so a multi-line program may follow the keyword, and a splice standing as an argument wears parentheses. With that, an object program stands wherever a Lean term stands: inside a pair, handed to List.map, sandwiched between Lean's id and a spliced function of the object language's own. One price of residence also shows here: declaring Unit a token of the object grammar reserves that spelling globally for the rest of the file, so a Lean-position ascription like (u : Unit) can no longer be written below the grammar, and the definitions here let Lean infer their types instead. The host lends its lexer, and the lease has terms.

#guard ((by_dtt let u : Unit = unit; u), (by_dtt (fun (x : Unit). x) unit))
    == ((), ())

#guard List.map (by_dtt fun (x : Unit). x) [(), (), ()] == [(), (), ()]

def sandwich := fun u =>
  id (applyTwice (by_dtt fun (x : Unit). x) u)

#guard sandwich () == ()

A language that does not look like Lean

The point of owning the grammar is that nothing forces it to resemble the host. A handful of productions and macro rules host a Chinese-keyword variant of the object language, just in time, inside the file. Two frame productions carry the binding forms, 设 x 类型为 A 其义为 t; u for let and 将 x 映射为 t for the lambda, with an annotated variant 将 (x 类型为 A) 映射为 t, and three tokens name the constants: 宇宙 for the universe, with 幺元类型 and 唯一元 for the unit type and its element. Words like 恒等 are a fourth kind of thing, names rather than keywords, about which more below:

namespace Zh

scoped syntax:max "宇宙" : dtt
scoped syntax:max "幺元类型" : dtt
scoped syntax:max "唯一元" : dtt
scoped syntax:10 "设 " dtt:max " 类型为 " dtt " 其义为 " dtt "; " dtt:10 : dtt
scoped syntax:10 "将 " dtt:max " 映射为 " dtt:10 : dtt
scoped syntax:10 "将 " "(" dtt:max " 类型为 " dtt ")" " 映射为 " dtt:10 : dtt

/-- A name slot holds an ordinary identifier or a declared name token;
either way, out comes the identifier it stands for. -/
def nameOf (x : TSyntax `dtt) : MacroM Ident :=
  match x with
  | `(dtt| $i:ident) => pure i
  | _ => do
    let .node _ _ #[.atom _ tok] := x.raw
      | Macro.throwUnsupported
    pure (mkIdent (.mkSimple tok))


def isIdeograph (ch : Char) : Bool :=
  0x4e00 <= ch.val && ch.val <= 0x9fff

open Lean.Parser in
/-- A maximal run of ideographs lexes as an ordinary identifier, unless the
word is a declared token: keywords stay keywords. -/
def zhIdentFn : ParserFn := fun c s =>
  let start := s.pos
  let s := takeWhile1Fn isIdeograph "Chinese identifier" c s
  if s.hasError then s
  else if (c.tokens.find? (c.extract start s.pos)).isSome then
    s.mkUnexpectedErrorAt "keyword" start
  else
    mkIdResult start none (.mkSimple (c.extract start s.pos)) true c s

open Lean.Parser in
def zhIdent : Parser :=
  { fn := zhIdentFn }

open PrettyPrinter in
@[combinator_formatter zhIdent]
def zhIdent.formatter : Formatter :=
  Formatter.identNoAntiquot.formatter

open PrettyPrinter in
@[combinator_parenthesizer zhIdent]
def zhIdent.parenthesizer : Parenthesizer :=
  Parenthesizer.identNoAntiquot.parenthesizer

/-- The bridge for a Lean-level word: the token becomes the identifier it
abbreviates. -/
def zhTermMacro : Macro := fun stx => do
  let x <- nameOf ⟨stx⟩
  pure x.raw

open Parser Elab Command in
/-- The category dispatch peeks the token table and gives up before trying
any production, so no production alone can admit new words. This command
rewires the dispatch for `dtt` alone: the standard parsers run first, so
every keyword wins, and a run of ideographs that matched nothing else
comes back as the identifier production. Any word is a name. -/
elab "zh_free_names" : command => do
  modifyEnv fun env =>
    categoryParserFnExtension.modifyState env fun prev => fun cat =>
      if cat != `dtt then prev cat
      else fun c s =>
        let iniSz := s.stackSize
        let iniPos := s.pos
        let s' := prev cat c s
        if !s'.hasError then s'
        else
          let s := s'.restore iniSz iniPos
          let s := zhIdentFn c s
          if s.hasError then s'
          else
            let s := s.mkNode ``dttIdent iniSz
            let s := { s with lhsPrec := Parser.maxPrec }
            match (parserExtension.getState c.env).categories.find? `dtt with
            | some catObj => Parser.trailingLoop catObj.tables c s
            | none => s

zh_free_names

open Elab Command in
/-- Abbreviate in Chinese: `略名 名 为 t` declares the abbreviation and
teaches the term grammar the word itself, so later uses need no «». -/
scoped elab "略名 " x:zhIdent " 为 " t:term : command => do
  let id : Ident := ⟨x.raw⟩
  elabCommand (<- `(abbrev $id:ident := $t))
  let kind := mkIdent (Name.mkSimple s!"zhTerm{id.getId.getString!}")
  elabCommand (<- `(scoped syntax:max (name := $kind) $(quote id.getId.getString!):str : term))
  elabCommand (<- `(attribute [macro $kind] zhTermMacro))

scoped macro "#推演 " decls:dttDecl* " |- " t:dtt : command =>
  `(#dtt_eval $decls* |- $t)

scoped syntax (name := zhGuard) (docComment)? "#验辞 " "in " command : command

scoped macro_rules
  | `($dc:docComment #验辞 in $c) => `($dc:docComment #guard_msgs in $c)

scoped macro_rules
  | `(dtt| 宇宙) => `(dtt| U)
  | `(dtt| 幺元类型) => `(dtt| Unit)
  | `(dtt| 唯一元) => `(dtt| unit)
  | `(dtt| 设 $x 类型为 $ty 其义为 $val; $body) => do
    let x <- nameOf x
    `(dtt| let $x : $ty = $val; $body)
  | `(dtt| 将 $x 映射为 $body) => do
    let x <- nameOf x
    `(dtt| fun $x. $body)
  | `(dtt| 将 ($x 类型为 $ty) 映射为 $body) => do
    let x <- nameOf x
    `(dtt| fun ($x:ident : $ty). $body)

end Zh

The design is the division of labor from chapter 3: the Chinese layer is macros, syntax to syntax, and the elaborator never learns Chinese. Because the rules are scoped, the layer switches on with open; because macro expansion preserves positions, an error in a 设 declaration points at the line the reader wrote; and because the productions extend the same category, mixing scripts in one term is not a stunt but the default. Two details earn their keep. The frame productions do not merely swap one keyword for another: 设 and 将 interleave their keywords between the moving pieces, so the declarations read as Chinese sentences, and the macro rewrite, being structural rather than textual, does not care where the pieces sit. And names, at last, need no door at all, though the reason took a fight to learn. Lean's tokenizer rejects CJK ideographs as identifier characters, and the category dispatch peeks the token table and gives up before trying any production, so neither an identifier nor any clever new production can admit a Chinese word. The layer's answer is one command: zh_free_names rewires the dispatch for dtt alone, standard parsers first, so every keyword keeps winning, and a run of ideographs that matched nothing else comes back as the identifier production. Any word is a name, no declaration anywhere. The same freedom one level up costs one line: 略名名为 t abbreviates at the Lean level and teaches the term grammar the word itself, and the layer aliases the judgment commands as #推演 and #验辞, so a program is written, checked, and pinned in one script:

open Zh

/-- info: let 恒等 : (A : U) -> A -> A = \A. \x. x; 恒等 : (A : U) -> A -> A -/
#验辞 in
#dtt_check |- 设 «恒等» 类型为 (A : 宇宙) -> A -> A 其义为 fun A. fun x. x; «恒等»

/-- info: let v : Unit = u; v : Unit -/
#验辞 in
#dtt_check (u : 幺元类型) |- 设 v 类型为 幺元类型 其义为 u; v

/-- info: unit : Unit -/
#验辞 in
#推演 |-
  设 «恒等» 类型为 (A : 宇宙) -> A -> A 其义为 将 A 映射为 将 x 映射为 x;
  设 w 类型为 幺元类型 其义为 «恒等» 幺元类型 唯一元;
  w

/--
info: let 再施 : (Unit -> Unit) -> Unit -> Unit = \f. \x. f (f x); 再施 : (Unit -> Unit) -> Unit -> Unit
-/
#验辞 in
#dtt_check |-
  设 «再施» 类型为 (幺元类型 -> 幺元类型) -> 幺元类型 -> 幺元类型
    其义为 将 f 映射为 将 x 映射为 f (f x);
  «再施»

/--
info: let 取先 : (A : U) -> A -> A -> A = \A. \x. \y. x; 取先 : (A : U) -> A -> A -> A
-/
#验辞 in
#dtt_check |-
  设 «取先» 类型为 (A : 宇宙) -> A -> A -> A
    其义为 将 A 映射为 将 x 映射为 将 y 映射为 x;
  «取先»

The splice composes with the layer, so object programs written in Chinese embed in ordinary Lean terms and run under #guard like any other value; the elaborator behind by_dtt expands the macros first and never notices the script. The closing definition is the composition in full: a Lean definition whose body is a multi-line Chinese program, dependently typed, its lambdas annotated because the backend demands domains. And the last guard runs the composition in both directions at once: Lean lends a Chinese name to Nat through its own escape hatch «...», and a polymorphic Chinese 再施 instantiates at it, doubling (· + 20) from 2 to land on 42:

#guard (by_dtt 设 v 类型为 幺元类型 其义为 唯一元; v) == ()

def zhProgram :=
  by_dtt
    设 «恒等» 类型为 (A : 宇宙) -> A -> A
      其义为 将 (A 类型为 宇宙) 映射为 将 (x 类型为 A) 映射为 x;
    «恒等» 幺元类型 唯一元

#guard zhProgram == ()

略名 «自然数» 为 Nat

#guard
  (by_dtt
    设 «再施» 类型为 (A : 宇宙) -> (A -> A) -> A -> A
      其义为 将 (A 类型为 宇宙) 映射为
        将 (f 类型为 A -> A) 映射为 将 (x 类型为 A) 映射为 f (f x);
    «再施»)
    自然数 (· + 20) 2 == 42

Scaled from a demonstration to a discipline, the same machinery carries natural language tactics: verbose-lean4, under Further reading, provides natural language tactics to teach mathematics using Lean 4, in French and in English, and the animated gif in its README shows the controlled language at work with its point-and-click interface.