Plans to add broader options for displaying type ascription

Stream: lean4

[Yutong Wang]

I noticed that some type ascriptions (Top.top, Bot.bot, Subtype.val as fas as I inspect) will not show after pp. They seems to be hidden no matter what pp.option are set.

This seems to be harmful for those circumstances where complete and compilable info is required (say extract_goal to build minimal working exp, or data extraction from mathlib).

So I wrote few delabs to handle this.

import Mathlib

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Top.top]
def delabTopAlwaysWithType : Delab := do
  let expr ←  getExpr
  if expr.isAppOf ``Top.top then
    let type ←  Meta.inferType expr
    let typeStx ←  delab type
    `((⊤ : $typeStx))
  else
    failure

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Top.top]
def delabBotAlwaysWithType : Delab := do
  let expr ←  getExpr
  if expr.isAppOf ``Bot.bot then
    let type ←  Meta.inferType expr
    let typeStx ←  delab type
    `((⊥ : $typeStx))
  else
    failure

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Subtype.val]
def delabSubtypeValAlwaysWithType : Delab := do
  let expr ←  getExpr
  if expr.isAppOf ``Subtype.val then
    let type ←  Meta.inferType expr
    let typeStx ←  delab type
    `((Subtype.val : $typeStx))
  else
    failure

Those delaborators work just fine in InfoView display. Might it be possible that we create a new option called always_show_type, so that all these scattered notations and delaborators can be properly handled?

[Aaron Liu]

import Mathlib

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Subtype.val]
def delabSubtypeValAlwaysWithType : Delab := do
  let expr ←  getExpr
  if expr.isAppOf ``Subtype.val then
    let type ←  Meta.inferType expr
    let typeStx ←  delab type
    `((Subtype.val : $typeStx))
  else
    failure

-- :(
/-- info: (Subtype.val✝ : ℕ) : ℕ -/
#guard_msgs in
#check @Subtype.val Nat (LT.lt 0) ⟨1, by decide⟩

[Yutong Wang]

Aaron Liu said:

import Mathlib

open Lean PrettyPrinter Delaborator SubExpr in
@[delab app.Subtype.val]
def delabSubtypeValAlwaysWithType : Delab := do
  let expr ←  getExpr
  if expr.isAppOf ``Subtype.val then
    let type ←  Meta.inferType expr
    let typeStx ←  delab type
    `((Subtype.val : $typeStx))
  else
    failure

-- :(
/-- info: (Subtype.val✝ : ℕ) : ℕ -/
#guard_msgs in
#check @Subtype.val Nat (LT.lt 0) ⟨1, by decide⟩

I guess this is working?

[Aaron Liu]

compare to

-- :)
/-- info: ⟨1, ⋯⟩.val : Nat -/
#guard_msgs in
#check @Subtype.val Nat (LT.lt 0) ⟨1, by decide⟩