Displaying explicit arguments

Stream: lean4

[Damiano Testa]

This is an issue related to the tactic extract_goal. Is there a way to get Lean to pretty print explicit and implicit arguments in the "same" way? Currently, Lean shows the binding brackets and the user-name of implicit arguments, but not of explicit ones.

Here is an example:

#check ∀ {i₁ : Nat} (e : Nat) {i₂ : Nat}, True
-- reality:     ∀ {i₁ : Nat}, Nat → ∀ {i₂ : Nat}, True : Prop
-- expectation: ∀ {i₁ : Nat} (e : Nat) {i₂ : Nat}, True : Prop

Same issue here, although I do not know if this is exactly the same path

import Mathlib.Tactic.RunCmd

open Lean Elab Tactic in
example : ∀ {i₁ : Nat} (e : Nat) {i₂ : Nat}, True := by
  run_tac do   -- ∀ {i₁ : Nat}, Nat → ∀ {i₂ : Nat}, True
    let g ← getMainGoal
    logInfo m!"{g}"

[Damiano Testa]

Similarly with groupings:

#check ∀ (e₁ : Nat) (e₂ : Nat) {i₁ : Nat} {i₂ : Nat}, True
-- reality:     Nat → Nat → ∀ {i₁ i₂ : Nat}, True : Prop
-- expectation: ∀ (e₁ e₂ : Nat) {i₁ i₂ : Nat}, True : Prop

[Floris van Doorn]

Something like this is definitely possible to code, but there is currently no option for it.
Note that #check <identifier> already does this: #check Prod

[Damiano Testa]

Floris, thank you for the comment! I'll try to look more into #check: when I tried before, I could extract much, but I'll give it another try!

The implementation that I have is !4#4595 and while I agree with the comment that it is very low-tech, I have not been able to leverage more of what is already available...