Equations
-
Lean.Elab.WF.packMutual preDefs = let _do_jp := fun y => do
let domain ← Lean.Elab.WF.mkNewDomain (Lean.Elab.WF.getDomains preDefs)
let a ← liftM (Lean.mkFreshUserName `_x)
Lean.Meta.withLocalDeclD a domain fun x => do
let codomain ← Lean.Elab.WF.mkNewCoDomain x preDefs
let type ← Lean.Meta.mkForallFVars #[x] codomain false true
let value ← Lean.Elab.WF.packValues x codomain preDefs
let newFn : Lean.Name := (Array.getOp preDefs 0).declName ++ `_mutual
let preDefNew : Lean.Elab.PreDefinition :=
let src := Array.getOp preDefs 0;
{ ref := src.ref, kind := src.kind, levelParams := src.levelParams, modifiers := src.modifiers,
declName := newFn, type := type, value := value }
Lean.Elab.addAsAxiom preDefNew
let value ←
Lean.Meta.transform value (fun e => pure (Lean.TransformStep.visit e))
(Lean.Elab.WF.post preDefs domain newFn)
let value ← Lean.Meta.mkLambdaFVars #[x] value false true
pure
{ ref := preDefNew.ref, kind := preDefNew.kind, levelParams := preDefNew.levelParams,
modifiers := preDefNew.modifiers, declName := preDefNew.declName, type := preDefNew.type,
value := value };
if (Array.size preDefs == 1) = true then pure (Array.getOp preDefs 0)
else do
let y ← pure PUnit.unit
_do_jp y