From 62363cb9438d8f7875227a180bbf618865675141 Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Tue, 14 Jan 2025 13:21:38 -0800
Subject: [PATCH] fix: Over-eager assertion of fvarId validity

---
 Pantograph/Frontend/MetaTranslate.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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