fix: Instantiation causes infinite loop #54

Merged
aniva merged 2 commits from output/expr into dev 2024-03-31 16:43:53 -07:00
2 changed files with 3 additions and 7 deletions
Showing only changes of commit e13b119ed1 - Show all commits

View File

@ -127,7 +127,7 @@ def exprEcho (expr: String) (options: @&Protocol.Options):
| .error e => return .error e
| .ok expr => pure expr
try
let type ← instantiateAll (← Lean.Meta.inferType expr)
let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr)
return .ok {
type := (← serialize_expression options type),
expr := (← serialize_expression options expr)
@ -171,9 +171,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
state.restoreMetaM
return {
root? := ← state.rootExpr?.mapM (λ expr => do
serialize_expression options (← instantiateAll expr)),
serialize_expression options (← unfoldAuxLemmas expr)),
parent? := ← state.parentExpr?.mapM (λ expr => do
serialize_expression options (← instantiateAll expr)),
serialize_expression options (← unfoldAuxLemmas expr)),
}
runMetaM metaM

View File

@ -18,10 +18,6 @@ namespace Pantograph
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
def instantiateAll (e: Lean.Expr) : Lean.MetaM Lean.Expr := do
let e ← unfoldAuxLemmas e
instantiateMVars (← Lean.Meta.whnf e)
--- Input Functions ---
/-- Read syntax object from string -/