From 589875a32a4f2e08e7259507f82ead240179c482 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 15 Dec 2024 23:21:34 +0100 Subject: [PATCH] chore: use builtin functions in equation computing (#248) --- DocGen4/Process/DefinitionInfo.lean | 15 +++++---------- 1 file changed, 5 insertions(+), 10 deletions(-) diff --git a/DocGen4/Process/DefinitionInfo.lean b/DocGen4/Process/DefinitionInfo.lean index 8d57bdb8..bf4fe63e 100644 --- a/DocGen4/Process/DefinitionInfo.lean +++ b/DocGen4/Process/DefinitionInfo.lean @@ -12,14 +12,6 @@ namespace DocGen4.Process open Lean Meta Widget -partial def stripArgs (e : Expr) (k : Expr → MetaM α) : MetaM α := - match e.consumeMData with - | Expr.forallE name type body bi => - let name := name.eraseMacroScopes - Meta.withLocalDecl name bi type fun fvar => do - stripArgs (Expr.instantiate1 body fvar) k - | _ => k e - def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do withOptions (tactic.hygienic.set . false) do lambdaTelescope v.value fun xs body => do @@ -28,9 +20,12 @@ def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do let type ← mkForallFVars xs type return type +def prettyPrintEquation (expr : Expr) : MetaM CodeWithInfos := + Meta.forallTelescope expr.consumeMData (fun _ e => prettyPrintTerm e) + def processEq (eq : Name) : MetaM CodeWithInfos := do let type ← (mkConstWithFreshMVarLevels eq >>= inferType) - stripArgs type prettyPrintTerm + prettyPrintEquation type def computeEquations? (v : DefinitionVal) : MetaM (Array CodeWithInfos) := do let eqs? ← getEqnsFor? v.name @@ -39,7 +34,7 @@ def computeEquations? (v : DefinitionVal) : MetaM (Array CodeWithInfos) := do let eqs ← eqs.mapM processEq return eqs | none => - let equations := #[← stripArgs (← valueToEq v) prettyPrintTerm] + let equations := #[← prettyPrintEquation (← valueToEq v)] return equations def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo := do