def
Lean.Elab.Structural.addSmartUnfoldingDefAux
(preDef : Lean.Elab.PreDefinition)
(recArgPos : Nat)
:
Equations
- Lean.Elab.Structural.addSmartUnfoldingDefAux preDef recArgPos = (fun visit => do let a ← visit preDef.value pure { ref := preDef.ref, kind := preDef.kind, levelParams := preDef.levelParams, modifiers := { docString? := none, visibility := Lean.Elab.Visibility.regular, isNoncomputable := false, recKind := Lean.Elab.RecKind.default, isUnsafe := false, attrs := #[] }, declName := Lean.Meta.mkSmartUnfoldingNameFor preDef.declName, type := preDef.type, value := a }) (Lean.Elab.Structural.addSmartUnfoldingDefAux.visit preDef recArgPos)
partial def
Lean.Elab.Structural.addSmartUnfoldingDefAux.visit
(preDef : Lean.Elab.PreDefinition)
(recArgPos : Nat)
(e : Lean.Expr)
:
def
Lean.Elab.Structural.addSmartUnfoldingDef
(preDef : Lean.Elab.PreDefinition)
(recArgPos : Nat)
:
Equations
- Lean.Elab.Structural.addSmartUnfoldingDef preDef recArgPos = do let a ← liftM (Lean.Meta.isProp preDef.type) if a = true then pure () else do let preDefSUnfold ← liftM (Lean.Elab.Structural.addSmartUnfoldingDefAux preDef recArgPos) Lean.Elab.addNonRec preDefSUnfold true