aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 12 Pull Requests 2 Packages Projects Releases Wiki Activity

fix(frontend): Capture local instances in MetaTranslate #242

Merged
aniva merged 4 commits from bug/meta-translate-local-instances into dev 2025-07-13 23:03:14 -07:00
Conversation 0 Commits 4 Files Changed 3 -1
1 changed files with 0 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 3bbbb14da6 - Show all commits

1
Pantograph/Frontend/MetaTranslate.lean
View File

@ -148,7 +148,6 @@ def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab
}) do }) do
let type := termInfo.expectedType?.get! let type := termInfo.expectedType?.get!
let lctx' ← translateLCtx let lctx' ← translateLCtx
--let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
let mvar ← Meta.withLCtx lctx' #[] do let mvar ← Meta.withLCtx lctx' #[] do
Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do Meta.withLocalInstances (lctx'.decls.toList.filterMap id) do
let type' ← translateExpr type let type' ← translateExpr type