Pretty-printing universal quantifier

Stream: lean4

[Martin C]

Hello,

I am trying to write macros for denoting universal/existential quantification in a custom logical syntax, and would like to reuse the ∀/∃ notations for that purpose. Here is a reduced version of what I have so far:

class Syntax where
  WFF : Type

  alwaysFalseWFF : WFF
  universal : forall {T}, (T -> WFF) -> WFF
  existential : forall {T}, (T -> WFF) -> WFF

open Syntax

notation:max "⊥" => alwaysFalseWFF

macro "∃ " xs:Lean.explicitBinders ", " Φ:term : term
  => Lean.expandExplicitBinders ``existential xs Φ

@[appUnexpander existential] def unexpandExistential :
  Lean.PrettyPrinter.Unexpander
| `($(_) fun $x:ident => ∃ $xs:binderIdent*, $Φ) =>
  `(∃ $x:ident $xs:binderIdent*, $Φ)
| `($(_) fun $x:ident => $Φ) => `(∃ $x:ident, $Φ)
| _ => throw ()

macro "∀ " xs:Lean.explicitBinders ", " Φ:term : term
  => Lean.expandExplicitBinders ``universal xs Φ

@[appUnexpander universal] def unexpandUniversal :
  Lean.PrettyPrinter.Unexpander
| `($(_) fun $x:ident => ∀ $xs:binderIdent*, $Φ) =>
  `(∀ $x:ident $xs:binderIdent*, $Φ)
| `($(_) fun $x:ident => $Φ) => `(∀ $x:ident, $Φ)
| _ => throw ()

#check fun [Syntax] => ∃ x y, ⊥
-- fun [Syntax] => ∃ x y, ⊥ : [inst : Syntax] → WFF
-- as expected

#check fun [Syntax] => ∀ x y, ⊥
-- fun [Syntax] => ∀ x, ∀ y, ⊥ : [inst : Syntax] → WFF
-- not as expected:
-- I would have liked to see
-- fun [Syntax] => ∀ x y, ⊥ : [inst : Syntax] → WFF
-- as in the existential case

The problem arises when pretty-printing universally quantified WFFs with multiple variables; while it works fine for the existential case, it doesn't for the universal case. Do you know why that is?

Thanks

Martin

[Sebastian Ullrich]

It looks like this is due to overloading the built-in syntax, which sounds like a bad idea to do. You should either choose a different symbol/variant or, if your embedded syntax is otherwise independent of term, use a separate syntax category as in https://leanprover.github.io/lean4/doc/metaprogramming-arith.html