Typechecking expressions in an arbitrary context

Stream: general

[Jannis Limperg]

Hey! For a tactic I'm writing, it would be useful to typecheck/normalise expressions in some context that isn't the current local context. I don't see a way to do that with the Lean primitives; any ideas?

[Mario Carneiro]

you are right that this is not easy. Are you looking for a fix or a workaround?

[Mario Carneiro]

The workaround is to clear everything, construct a pi type and then use intro

[Jannis Limperg]

I imagine the fix wouldn't be easy, so I'll try the workaround for now. Thanks a lot!

[Mario Carneiro]

open tactic
example (x y : ℕ) : x = y :=
by do
  gs ← get_goals,
  set_goals [],
  e ← mk_mvar,
  set_goals [e],
  e ← to_expr ``(∀ my new ctx: ℕ, true) >>= mk_meta_var,
  set_goals [e],
  intros,
  e ← target,
  trace_state,
  set_goals gs

By the way, if you replace gs with e :: gs on the last line, lean segfaults

[Jannis Limperg]

Awesome, thanks! (And the segfault is why I'm not touching the C++.)

[Bryan Gin-ge Chen]

Is this one of the known crashes, or a new one?

[Mario Carneiro]

I would guess a new one. Working with expressions in unrelated local contexts in the same tactic state appears to be poorly supported, and it's also not a common thing to do from lean