check output

Stream: lean4

[Patrick Massot]

Is there any reason why

variable (f : Nat → Nat)

#check f

gives the expected output Nat → Nat but

def addOne : Nat → Nat := fun x ↦ x + 1

#check addOne

prints a weird addOne (a✝ : Nat) : Nat?

[Kyle Miller]

There's a special case in #check where if the expression is a constant then it uses a different pretty printer that tries to format it like a function definition.

[Eric Wieser]

#check (addOne) gives the behavior you expect

[Kyle Miller]

If you do #check @addOne you can trick it into not doing that

[Kyle Miller]

Parentheses instantiate implicit arguments with metavariables, which might not be what you want.

[Patrick Massot]

But why does #check do that to me?

[Eric Wieser]

Because of this thread:

Sebastian Ullrich said:

In lean4#1943, I made a suggestion not directly related to the PR:

In fact I would probably go further and just make #check $n:ident a semantically separate command that shows the signature of n without elaboration - I can't be the only one that usually starts with #check toString and then only remembers to add the @ on the second try.

How do people use #check around here? Would it be a welcome change if #check toString printed

ToString.toString.{u} {α : Type u} [self : ToString α] (a : α) : String

(using the fancy new signature pretty printer) instead of

toString : ?m.1632 → String

even if it is not perfectly consistent with the more general meaning "show type of this term" of #check?

[Patrick Massot]

Well, I guess I understand how it is useful in real situations. It's simply inconvenient in early teaching.

[Kyle Miller]

Here's an override using the standard type signature rather than the fancy one:

open Lean Elab Command Meta in
elab_rules : command
  | `(command| #check%$tk $term) => withoutModifyingEnv <| runTermElabM fun _ => Elab.Term.withDeclName `_check do
    if let `($_:ident) := term then
      try
        for c in (← resolveGlobalConstWithInfos term) do
          let decl ← getConstInfo c
          addCompletionInfo <| .id term c (danglingDot := false) {} none
          logInfoAt tk m!"{c} : {decl.type}"
          return
      catch _ => pure ()  -- identifier might not be a constant but constant + projection
    let e ← Term.elabTerm term none
    Term.synthesizeSyntheticMVarsNoPostponing
    let e ← Term.levelMVarToParam (← instantiateMVars e)
    let type ← inferType e
    if e.isSyntheticSorry then
      return
    logInfoAt tk m!"{e} : {type}"

#check addOne
-- addOne : Nat → Nat

[Kyle Miller]

Maybe the real #check could have an option for how fancy it should be?

[Gabriel Ebner]

You can override the command much more easily. :smile:

macro_rules
  | `(#check ($_)) => Lean.Macro.throwUnsupported
  | `(#check%$tk $term) => `(#check%$tk ($term))

[Kyle Miller]

That gives different output -- it instantiates the implicit arguments

[Kyle Miller]

macro_rules
  | `(#check @$_) => Lean.Macro.throwUnsupported
  | `(#check $term) => `(#check @$term)

This would be closer, but it prepends @ to the name in the output

[Mario Carneiro]

arguably it is more correct/consistent to put the @ on the name

[Eric Wieser]

Lean3 doesn't do so when you hover over a name in the editor

[Mario Carneiro]

yes but that's the signature pretty printer, which as we have established has its own rules

[Mario Carneiro]

the desired behavior here seems to be expr : type and for that you want to print expr in such a way that it is at least plausibly re-parseable

[Mario Carneiro]

which means putting @ if there is an unapplied implicit arg