Documentation

Lean.Elab.PreDefinition.Structural.Eqns

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

Type

recArgPos : Nat

instance Lean.Elab.Structural.instInhabitedEqnInfo :

Inhabited Lean.Elab.Structural.EqnInfo

Equations

Lean.Elab.Structural.instInhabitedEqnInfo = { default := { toEqnInfoCore := default, recArgPos := default } }

def Lean.Elab.Structural.mkEqns (info : Lean.Elab.Structural.EqnInfo) :

Lean.MetaM (Array Lean.Name)

Equations

Lean.Elab.Structural.mkEqns info = Lean.withOptions (fun a => Lean.Option.set a Lean.Meta.tactic.hygienic false) do 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 info.toEqnInfoCore.declName us) xs) body let goal ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar target Lean.Name.anonymous Lean.Elab.Eqns.mkEqnTypes #[info.toEqnInfoCore.declName] (Lean.Expr.mvarId! goal)) let a ← Lean.getEnv let baseName : Lean.Name := Lean.Elab.Eqns.mkBaseNameFor a info.toEqnInfoCore.declName 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.structural.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.Structural.mkProof info.toEqnInfoCore.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.Structural.eqnInfoExt :

Lean.MapDeclarationExtension Lean.Elab.Structural.EqnInfo

def Lean.Elab.Structural.registerEqnsInfo (preDef : Lean.Elab.PreDefinition) (recArgPos : Nat) :

Lean.CoreM Unit

Equations

Lean.Elab.Structural.registerEqnsInfo preDef recArgPos = Lean.modifyEnv fun env => Lean.MapDeclarationExtension.insert Lean.Elab.Structural.eqnInfoExt env preDef.declName { toEqnInfoCore := { declName := preDef.declName, levelParams := preDef.levelParams, type := preDef.type, value := preDef.value }, recArgPos := recArgPos }

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

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

Equations

Lean.Elab.Structural.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.Structural.eqnInfoExt env declName with | some info => do let eqs ← Lean.Elab.Structural.mkEqns 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.Structural.getUnfoldFor? (declName : Lean.Name) :

Lean.MetaM (Option Lean.Name)

Equations

Lean.Elab.Structural.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.Structural.eqnInfoExt env declName)