aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 13 Pull Requests 4 Packages Projects Releases Wiki Activity

chore: Version 0.3 #136

Open
aniva wants to merge 487 commits from dev into main
pull from: dev
merge into: aniva:main
Conversation 0 Commits 487 Files Changed 52 +2 -2
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit e9c9548f17 - Show all commits

2
Pantograph/Environment.lean
View File

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

2
Pantograph/Serial.lean
View File

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