Variant of #check command that unfold let expression

Stream: Is there code for X?

[Asei Inoue]

I ask this out of curiosity, but would it be possible to create a variant of the #check command that would expand let expressions?

For example, #check (let x := 1; x) does not show up as 1 : Nat, but could it be made to show up as 1 : Nat?

[Aaron Liu]

yes

[Asei Inoue]

How can I implement this?

[Aaron Liu]

write a wrapper for #check that zeta-reduces its argument first

[Aaron Liu]

import Lean

open Lean Meta Elab Term Command

elab tk:"#checkz" t:term : command => do
  -- copied from the `#check` command
  withoutModifyingEnv <| runTermElabM fun _ => withDeclName `_check do
  let e ← elabTerm t none
  let e ← zetaReduce e
  synthesizeSyntheticMVarsNoPostponing (ignoreStuckTC := true)
  -- Users might be testing out buggy elaborators. Let's typecheck before proceeding:
  withRef tk <| check e
  let e ← levelMVarToParam (← instantiateMVars e)
  if e.isSyntheticSorry then
    return
  let type ← inferType e
  logInfoAt tk m!"{e} : {type}"

#checkz let x := 1; x

[Damiano Testa]

There is also #simp that can be useful in similar situations.

[Eric Wieser]

Or you could use letI here

[Asei Inoue]

Thank you!!