lean

How to include special characters like ≅ into "UnexpandM Syntax" syntax quotations?

If I define a macro which rewrites ab ≅ cd into Congruent a b c d (where Congruent takes four terms of a given type), executing the #check command will always produce the output of the macro (i.e., Congruent a b c d).

I tried using the Unexpander to pretty print the syntax but was unable to include the ≅ symbol into the syntax quotations.

import Lean

inductive Point : Type

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

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

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 ()
/- Throws the following error:
unexpected token '≅'; expected ')' or '|'
-/

variable (a b c d : Point)

#check ab ≅ cd

I tried enclosing ≅ in French brackets « » but it produces the following:

#check Congruent a b c d -- ab ≅✝ cd : Prop

I also attempted converting ≅ into a literal using let cong := mkIdent (Name.mkStr1 "≅") and then place in syntax quotations ($ab $cong $cd) but it prints the symbol with French brackets.

#check Congruent a b c d -- ab «≅» cd : Prop

I feel that I am missing out on something but I am unsure as to what it is.

Solution

  • After some trial and error, I was able to figure out the solution myself. Apparently it is necessary to specify the syntax categories of newly defined variables within the unexpander function for Lean to match the syntax quotation with the previously defined syntax. In my case this is $ab:ident instead of just $ab.

    Here is the corrected code snippet:

    import Lean

inductive Point : Type

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

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

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:ident ≅ $cd:ident)
  | _ => throw ()

variable (a b c d : Point)

#check Congruent a b c d -- ab ≅ cd : Prop