MVars to FVars

Stream: Is there code for X?

[Joachim Breitner]

Given a array of Lean.Exprs that contain MVars, is there an easy way to turn all MVars into local declarations (assigned ones as let declarations, or instantiated if that’s easier; unassigned one as fresh variables).

(A bit like abstractMVars followed by lambdaTelescope, but visiting more than one expression).

[Joachim Breitner]

Maybe cargo-culting abstractMVars is the way to go:

def mvarsToContext {α} (es : Array Expr) (e : Expr) (k : Expr → MetaM α) : MetaM α := do
  let e ← instantiateMVars e
  let mut s := { mctx := (← getMCtx), lctx := (← getLCtx), ngen := (← getNGen), abstractLevels := false }
  for e' in es do
    (_, s) := AbstractMVars.abstractExprMVars e' s
  let (e, s') := AbstractMVars.abstractExprMVars e s
  s := s'
  setNGen s.ngen
  setMCtx s.mctx
  let e := s.lctx.mkForall s.fvars e
  forallBoundedTelescope e (s.fvars.size) fun _ e => k e