check Exists.intro

Stream: lean4

[Patrick Massot]

Does anyone know how to get #check Exists.intro to use the existential notation? This is for teaching pruposes.

[Kyle Miller]

This is what it's outputting:

Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p

and this is what Patrick would want to see:

Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : ∃ x, p x

[Kyle Miller]

The issue is that the app_unexpander is looking for Exists fun $x => $body, and it doesn't know about Exists $p. For that, it'd need to generate a fresh name disjoint from the identifiers that appear in p, which seems doable from the UnexpandM monad. (Though there's a comment "unexpanders should not need to introduce new names" in the code.)

[Mario Carneiro]

@[app_unexpander Exists] def unexpandExists' : Lean.PrettyPrinter.Unexpander
  | `($(_) fun $_* => $_) => throw ()
  | `($(_) $p) => let x := Lean.mkIdent `x; `(∃ $x:ident, $p $x)
  | _ => throw ()

#check Exists.intro

[Mario Carneiro]

I cheated re: introducing new names, just don't use this for a predicate named x

[Patrick Massot]

Thanks!

[Ruben Van de Velde]

You could use ᾰ