構造体(structure)のフィールドを部分的に更新するdo構文を作る。macro_rules コマンド使用例

Zulip: notation for unpacking structures and field assignment

mkIdentFrom などの良い使用例になっている。本文で紹介するためには、私が実装の詳細をきちんと理解する必要がある。

import Lean

open Lean Parser

macro_rules
| `(doElem| $x:ident := $val) => do
  let .str n f := x.getId | Macro.throwUnsupported
  if n == .anonymous then Macro.throwUnsupported
  let o := mkIdentFrom x n
  let field := mkIdentFrom x (Name.mkSimple f)
  `(doElem| $o:ident := {$o with $field:ident := $val})

#guard show Bool from Id.run do
  let mut s := (1,2)
  s.fst := 3
  s == (3, 2)

Start with the linked Zulip discussion and the shown macro_rules example, then inspect the uses of mkIdentFrom and the #guard example. Document this partial structure-field update do syntax in the relevant book section, including the macro_rules usage. Done when the implementation details and runnable example are clearly explained.