Lean4元编程求助：将双字符标识符拆分为两个已有标识符

完整实现代码 #

import Lean

open Lean

-- 定义split宏，将双字符标识符拆分为两个单字符变量的等式
macro "split" id:ident : term => do
  let name := id.getId
  let s := name.toString
  -- 校验输入必须是双字符标识符
  unless s.length == 2 do
    throwError "split expects a two-character identifier (e.g. `ab`)"
  -- 拆分字符并生成单字符标识符
  let c1 := s.get! 0
  let c2 := s.get! 1
  let id1 := mkIdent (Name.mkStr1 c1)
  let id2 := mkIdent (Name.mkStr1 c2)
  -- 生成 `a = b` 形式的表达式（等价于 `Eq a b`）
  `($id1 = $id2)

-- 测试示例
variable (a b : Type')

#check split ab -- 输出：a = b : Prop

关键步骤说明 #

1. 提取标识符名称：通过id.getId获取输入标识符的Name类型，再用Name.toString转为字符串，方便拆分字符。
2. 合法性校验：强制输入必须是双字符标识符，不符合则抛出明确错误提示。
3. 生成新标识符：用Name.mkStr1将单个字符转为Name，再通过mkIdent生成对应的标识符语法节点（Lean.TSyntax ident`）。
4. 构造目标表达式：利用Lean的引号语法 ($id1 = $id2) 直接生成等式表达式，自动转换为Lean.MacroM (Lean.TSyntax term)类型，满足宏的返回要求。

对您尝试的补充说明 #

您之前尝试将标识符转为List Char再生成Name的思路是对的，核心缺失的是用mkIdent将Name转为合法的语法节点，再通过引号语法嵌入到目标表达式中。Lean的宏系统要求返回的是语法树节点，而非原始的Name或字符串，mkIdent和引号语法正是完成这一步的关键工具。

关于您示例的修正 #

您原示例中的#check Eq (split ab)会导致类型错误，因为split ab已经展开为a = b（类型为Prop），而Eq需要的是两个同类型的项作为参数。正确的用法是直接#check split ab，它会输出a = b : Prop，与您期望的结果一致。

扩展说明 #

如果需要更复杂的逻辑（比如处理更多字符、自定义输出形式），可以改用elab代替macro，elab允许您直接操作经过预处理的表达式，灵活性更高，但对于纯语法转换场景，macro足够轻量高效。

内容的提问来源于stack exchange，提问作者owlattack22