fix: reintroduce basic definition lemmas

Closes: #155
main
Henrik Böving 2023-10-08 11:33:27 +02:00
parent 3a9cfabe58
commit 402cfda104
1 changed files with 27 additions and 8 deletions

View File

@ -19,6 +19,14 @@ partial def stripArgs (e : Expr) : Expr :=
stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩)) stripArgs (Expr.instantiate1 body (mkFVar ⟨name⟩))
| _ => e | _ => e
def valueToEq (v : DefinitionVal) : MetaM Expr := withLCtx {} {} do
withOptions (tactic.hygienic.set . false) do
lambdaTelescope v.value fun xs body => do
let us := v.levelParams.map mkLevelParam
let type ← mkEq (mkAppN (Lean.mkConst v.name us) xs) body
let type ← mkForallFVars xs type
return type
def processEq (eq : Name) : MetaM CodeWithInfos := do def processEq (eq : Name) : MetaM CodeWithInfos := do
let type ← (mkConstWithFreshMVarLevels eq >>= inferType) let type ← (mkConstWithFreshMVarLevels eq >>= inferType)
let final := stripArgs type let final := stripArgs type
@ -30,7 +38,18 @@ def DefinitionInfo.ofDefinitionVal (v : DefinitionVal) : MetaM DefinitionInfo :=
let isNonComputable := isNoncomputable (← getEnv) v.name let isNonComputable := isNoncomputable (← getEnv) v.name
try try
let eqs? ← getEqnsFor? v.name let eqs? ← getEqnsFor? v.name
let equations ← eqs?.mapM (·.mapM processEq) match eqs? with
| some eqs =>
let equations ← eqs.mapM processEq
return {
toInfo := info,
isUnsafe,
hints := v.hints,
equations,
isNonComputable
}
| none =>
let equations := #[← prettyPrintTerm <| stripArgs (← valueToEq v)]
return { return {
toInfo := info, toInfo := info,
isUnsafe, isUnsafe,