localHyps not getting have statments

Stream: general

[Frederick Pu]

example (x : Nat) : x = x := by
  have : x = x := rfl
  run_tac do
    let womp ← Lean.Elab.Tactic.getMainGoal
    -- IO.println (← Lean.getLocalHyps).size
    IO.println (← Lean.MonadLCtx.getLCtx).size
    for hyp in ← Lean.getLocalHyps do
      IO.println (← hyp.fvarId!.getType)
    -- Nat

  exact this

as you can see in the above the x = x have statement isn't showing up in the getLocalHyps call

[Eric Wieser]

docs#Lean.Elab.Tactic.withMainContext

[Frederick Pu]

oh thanks

[Eric Wieser]

Without that you get the local context at the very start of the by block

[Frederick Pu]

also how do you print an expr in raw form

[Frederick Pu]

so i can see which constructors are being applied and stuff

[Jakub Nowak]

s!"{e}" or e.dbgToString.

[Eric Wieser]

m!"{repr e}" I think?

[Frederick Pu]

thanks so much!!!