fix: unfoldAuxLemma should be coreM

This commit is contained in:
Leni Aniva 2024-03-31 15:40:14 -07:00
parent e13b119ed1
commit 6235d61433
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
2 changed files with 2 additions and 2 deletions

View File

@ -64,7 +64,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
else .none,
valueDependency? := ← if args.dependency?.getD false
then info.value?.mapM (λ e => do
let e ← (unfoldAuxLemmas e).run'
let e ← unfoldAuxLemmas e
pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
else pure (.none),
module? := module?

View File

@ -15,7 +15,7 @@ def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxL
namespace Pantograph
/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
def unfoldAuxLemmas (e : Lean.Expr) : Lean.MetaM Lean.Expr := do
def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
--- Input Functions ---