types of tombstoned hypotheses?

Stream: lean4

[Scott Morrison]

In

def mkConst' (constName : Name) : MetaM Expr := do
  return mkConst constName (← (← getConstInfo constName).levelParams.mapM fun _ => mkFreshLevelMVar)

def getLocalHyps : MetaM (Array Expr) := do
  let mut hs := #[]
  for d in ← getLCtx do
    if !d.isAuxDecl then hs := hs.push d.toExpr
  return hs

def foo (g : MVarId) : MetaM MVarId := do
  let [g] ← g.apply (← mkConst' ``Not.intro) | failure
  let (_, g) ← g.intro1P
  return g

def bar (g : MVarId) : MetaM (List MVarId) := do
  let g ← foo g
  g.withContext do
    let hyps ← getLocalHyps
    logInfo m!"{hyps}"
    let types ← hyps.mapM inferType
    logInfo m!"{types}"
    return [g]

elab "bar" : tactic => do liftMetaTactic bar

example (h : 0 < 1) : ¬ 7 < 3 := by
  bar
  admit

At bar it prints:

[h, a✝]
[0 < 1, ?a]

but I was expecting it to print

[h, a✝]
[0 < 1, 7 < 3]

What is happening / what should I be doing differently?

[Gabriel Ebner]

I think you're just missing an instantiateMVars.

BTW, these days you should be using d.isImplementationDetail instead of d.isAuxDecl.