app_unexpander

[app_unexpander] 属性を付与すると、関数適用 f a₁ a₂ ... aₙ の #check コマンドおよび infoview での表示のされ方を変更することができます。

/-- 人に挨拶をする関数 -/
def greet (x : String) := s!"Hello, {x}!"


/-- すべての挨拶の表示を強制的に hello world に変えてしまう -/
@[app_unexpander greet]
def unexpGreet : Lean.PrettyPrinter.Unexpander
  | `(greet $x) => `("hello world")
  | _ => throw ()

-- #check の表示が上書きされて変わる
/-- info: "hello world" : String -/
#guard_msgs in
  #check greet "Alice"

-- #eval の表示は変わらない
/-- info: "Hello, Alice!" -/
#guard_msgs in
  #eval greet "Alice"

より実用的な例として、集合の内包記法の表示のされ方を制御する例が挙げられます。

/-- α を全体集合として、その部分集合の全体。
α の部分集合と α 上の述語を同一視していることに注意。 -/
def Set (α : Type) := α → Prop

variable {α : Type}

/-- 述語 `p : α → Prop` に対応する集合 -/
def setOf {α : Type} (p : α → Prop) : Set α := p

/-- 内包表記 `{ x : α | p x }` の `x : α` の部分のための構文。
`: α` の部分はあってもなくてもよいので `( )?` で囲っている。-/
syntax extBinder := ident (" : " term)?

/-- 内包表記 `{ x : α | p x }` の `{ | }` の部分のための構文。 -/
syntax (name := setBuilder) "{" extBinder " | " term "}" : term

/-- 内包表記の意味をマクロとして定義する -/
macro_rules
  | `({ $x:ident : $type | $p }) => `(setOf (fun ($x : $type) => $p))
  | `({ $x:ident | $p }) => `(setOf (fun ($x : _) => $p))

-- 内包表記が使えるようになったが、コマンドの出力や infoview では
-- いま定義した記法が使われないという問題がある
/-- info: setOf fun n => ∃ m, n = 2 * m : Set Nat -/
#guard_msgs in
  #check {n : Nat | ∃ m, n = 2 * m}

/-- infoview やコマンドの出力でも内包表記を使用するようにする -/
@[app_unexpander setOf]
def setOf.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ fun $x:ident => $p) => `({ $x:ident | $p })
  | `($_ fun ($x:ident : $ty:term) => $p) => `({ $x:ident : $ty:term | $p })
  | _ => throw ()

-- 正常に動作することを確認

/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/
#guard_msgs in
  #check {n | ∃ m, n = 2 * m}

/-- info: {n | ∃ m, n = 2 * m} : Set Nat -/
#guard_msgs in
  #check {n : Nat | ∃ m, n = 2 * m}