diff --git a/Pantograph/Frontend/MetaTranslate.lean b/Pantograph/Frontend/MetaTranslate.lean index bd3568d..c6592d2 100644 --- a/Pantograph/Frontend/MetaTranslate.lean +++ b/Pantograph/Frontend/MetaTranslate.lean @@ -68,7 +68,8 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do match e with | .fvar fvarId => let .some fvarId' := state.fvarMap[fvarId]? | panic! s!"FVar id not registered: {fvarId.name}" - assert! (← getLCtx).contains fvarId' + -- Delegating this to `Meta.check` later + --assert! (← getLCtx).contains fvarId' return .done $ .fvar fvarId' | .mvar mvarId => do -- Must not be assigned