如何在Lean的UnexpandM语法引用中包含≅等特殊字符？

问题原因 #

核心问题在于Lean的语法引用（`(...)）无法直接识别未注册的符号≅——默认情况下Lean的term语法范畴不包含该符号，导致反展开器里的$ab ≅ $cd被判定为非法语法。

解决方案 #

要让反展开器正确生成ab ≅ cd的美化输出，需先将≅注册为Lean语法系统中合法的term级符号，再调整反展开器实现。

完整代码示例 #

import Lean

inductive Point : Type

inductive Congruent : Point -> Point -> Point -> Point -> Prop

-- 第一步：注册 `≅` 相关语法，让Lean识别 `ident ≅ ident` 为合法term
declare_syntax_cat congruence_expr
syntax ident " ≅ " ident : congruence_expr
syntax congruence_expr : term

-- 第二步：定义宏，将 `ab ≅ cd` 展开为 `Congruent a b c d`
macro ab:ident " ≅ " cd:ident : term =>
  match ab.getId.toString.toList with
    | [a, b] =>
      match cd.getId.toString.toList with
      | [c, d] =>
        let a := Lean.mkIdent (Lean.Name.mkStr1 ("".push a))
        let b := Lean.mkIdent (Lean.Name.mkStr1 ("".push b))
        let c := Lean.mkIdent (Lean.Name.mkStr1 ("".push c))
        let d := Lean.mkIdent (Lean.Name.mkStr1 ("".push d))
        `(Congruent $a $b $c $d)
      | _ => Lean.Macro.throwUnsupported
    | _ => Lean.Macro.throwUnsupported

-- 第三步：定义反展开器，将 `Congruent a b c d` 还原为 `ab ≅ cd`
open Lean PrettyPrinter Delaborator SubExpr in
@[app_unexpander Congruent]
def unexpandCongruent : Unexpander
  | `(Congruent $a:ident $b:ident $c:ident $d:ident) => do
    let ab := mkIdent (Name.mkStr1 (a.getId.toString ++ b.getId.toString))
    let cd := mkIdent (Name.mkStr1 (c.getId.toString ++ d.getId.toString))
    `($ab ≅ $cd)
  | _ => throw ()

variable (a b c d : Point)

#check ab ≅ cd -- 现在输出为：ab ≅ cd : Prop

关键说明 #

1. 语法注册：通过declare_syntax_cat创建自定义语法范畴congruence_expr，将ident " ≅ " ident纳入该范畴后并入term语法，让Lean解析器认可ab ≅ cd是合法表达式。
2. 反展开器兼容：注册语法后，语法引用$ab ≅ $cd可被正确解析，反展开器能生成目标美化格式，#check命令会显示ab ≅ cd而非原始的Congruent a b c d。

若不想额外注册语法范畴，也可手动构造Syntax节点替代语法引用，示例如下：

open Lean PrettyPrinter Delaborator SubExpr in
@[app_unexpander Congruent]
def unexpandCongruent : Unexpander
  | `(Congruent $a:ident $b:ident $c:ident $d:ident) => do
    let ab := mkIdent (Name.mkStr1 (a.getId.toString ++ b.getId.toString))
    let cd := mkIdent (Name.mkStr1 (c.getId.toString ++ d.getId.toString))
    -- 手动构造包含≅的Syntax节点
    return Syntax.node `term #[ab.raw, Syntax.atom " ≅ ", cd.raw]
  | _ => throw ()

这种方式跳过语法注册，直接生成符合要求的语法树，同样能实现美化输出。

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