Documentation

Lean.Elab.PreDefinition.WF.Eqns

structure Lean.Elab.WF.EqnInfo extends Lean.Elab.Eqns.EqnInfoCore :

Type

declNames : Array Lean.Name
declNameNonRec : Lean.Name

instance Lean.Elab.WF.instInhabitedEqnInfo :

Inhabited Lean.Elab.WF.EqnInfo

Equations

Lean.Elab.WF.instInhabitedEqnInfo = { default := { toEqnInfoCore := default, declNames := default, declNameNonRec := default } }

def Lean.Elab.WF.mkEqns (declName : Lean.Name) (info : Lean.Elab.WF.EqnInfo) :

Lean.MetaM (Array Lean.Name)

Equations

Lean.Elab.WF.mkEqns declName info = Lean.withOptions (fun a => Lean.Option.set a Lean.Meta.tactic.hygienic false) do let a ← Lean.getEnv let baseName : Lean.Name := Lean.Elab.Eqns.mkBaseNameFor a declName let eqnTypes ← Lean.Meta.withNewMCtxDepth (Lean.Meta.lambdaTelescope info.toEqnInfoCore.value fun xs body => let us := List.map Lean.mkLevelParam info.toEqnInfoCore.levelParams; do let target ← Lean.Meta.mkEq (Lean.mkAppN (Lean.mkConst declName us) xs) body let goal ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar target Lean.Name.anonymous Lean.Elab.Eqns.mkEqnTypes info.declNames (Lean.Expr.mvarId! goal)) let thmNames : Array Lean.Name := #[] let r ← let col := { start := 0, stop := Array.size eqnTypes, step := 1 }; forIn col thmNames fun i r => let thmNames := r; let type := Array.getOp eqnTypes i; let cls := `Elab.definition.wf.eqns; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Array Lean.Name → Unit → Lean.MetaM (ForInStep (Array Lean.Name)) := fun thmNames y => let name := baseName ++ Lean.Name.appendIndexAfter `_eq (i + 1); let thmNames := Array.push thmNames name; do let value ← Lean.Elab.WF.mkProof declName type Lean.addDecl (Lean.Declaration.thmDecl { toConstantVal := { name := name, levelParams := info.toEqnInfoCore.levelParams, type := type }, value := value }) pure (ForInStep.yield thmNames) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData (Array.getOp eqnTypes i) ++ Lean.toMessageData "") _do_jp thmNames y else do let y ← pure PUnit.unit _do_jp thmNames y let x : Array Lean.Name := r let thmNames : Array Lean.Name := x pure thmNames

constant Lean.Elab.WF.eqnInfoExt :

Lean.MapDeclarationExtension Lean.Elab.WF.EqnInfo

def Lean.Elab.WF.registerEqnsInfo (preDefs : Array Lean.Elab.PreDefinition) (declNameNonRec : Lean.Name) :

Lean.CoreM Unit

Equations

Lean.Elab.WF.registerEqnsInfo preDefs declNameNonRec = let declNames := Array.map (fun a => a.declName) preDefs; Lean.modifyEnv fun env => Array.foldl (fun env preDef => Lean.MapDeclarationExtension.insert Lean.Elab.WF.eqnInfoExt env preDef.declName { toEqnInfoCore := { declName := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value }, declNames := declNames, declNameNonRec := declNameNonRec }) env preDefs 0 (Array.size preDefs)

def Lean.Elab.WF.getEqnsFor? (declName : Lean.Name) :

Lean.MetaM (Option (Array Lean.Name))

Equations

Lean.Elab.WF.getEqnsFor? declName = do let env ← Lean.getEnv match Std.PersistentHashMap.find? (Lean.EnvExtension.getState Lean.Elab.Eqns.eqnsExt env).map declName with | some eqs => pure (some eqs) | x => match Lean.MapDeclarationExtension.find? Lean.Elab.WF.eqnInfoExt env declName with | some info => do let eqs ← Lean.Elab.WF.mkEqns declName info Lean.modifyEnv fun env => Lean.EnvExtension.modifyState Lean.Elab.Eqns.eqnsExt env fun s => { map := Std.PersistentHashMap.insert s.map declName eqs } pure (some eqs) | x => pure none

def Lean.Elab.WF.getUnfoldFor? (declName : Lean.Name) :

Lean.MetaM (Option Lean.Name)

Equations

Lean.Elab.WF.getUnfoldFor? declName = do let env ← Lean.getEnv Lean.Elab.Eqns.getUnfoldFor? declName fun x => Option.map (fun a => a.toEqnInfoCore) (Lean.MapDeclarationExtension.find? Lean.Elab.WF.eqnInfoExt env declName)