def
Lean.Elab.Structural.mkBRecOn
(recFnName : Lean.Name)
(recArgInfo : Lean.Elab.Structural.RecArgInfo)
(value : Lean.Expr)
:
Equations
- Lean.Elab.Structural.mkBRecOn recFnName recArgInfo value = let cls := `Elab.definition.structural; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Structural.M Lean.Expr := fun y => do let a ← liftM (Lean.Meta.inferType value) let type : Lean.Expr := Lean.Expr.headBeta a let major : Lean.Expr := Array.getOp recArgInfo.ys recArgInfo.pos let otherArgs : Array Lean.Expr := Array.filter (fun y => y != major && !Array.contains recArgInfo.indIndices y) recArgInfo.ys 0 (Array.size recArgInfo.ys) let cls : Lean.Name := `Elab.definition.structural let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Structural.M Lean.Expr := fun y => do let motive ← liftM (Lean.Meta.mkForallFVars otherArgs type false true) let brecOnUniv ← liftM (Lean.Meta.getLevel motive) let cls : Lean.Name := `Elab.definition.structural let a ← Lean.isTracingEnabledFor cls let _do_jp : Lean.Level → Unit → Lean.Elab.Structural.M Lean.Expr := fun brecOnUniv y => let useBInductionOn := recArgInfo.reflexive && brecOnUniv == Lean.levelZero; let _do_jp := fun brecOnUniv y => do let motive ← liftM (Lean.Meta.mkLambdaFVars (Array.push recArgInfo.indIndices major) motive false true) let cls : Lean.Name := `Elab.definition.structural let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Structural.M Lean.Expr := fun y => let brecOn := if useBInductionOn = true then Lean.mkConst (Lean.mkBInductionOnName recArgInfo.indName) recArgInfo.indLevels else Lean.mkConst (Lean.mkBRecOnName recArgInfo.indName) (brecOnUniv :: recArgInfo.indLevels); let brecOn := Lean.mkAppN brecOn recArgInfo.indParams; let brecOn := Lean.mkApp brecOn motive; let brecOn := Lean.mkAppN brecOn recArgInfo.indIndices; let brecOn := Lean.mkApp brecOn major; do liftM (Lean.Meta.check brecOn) let brecOnType ← liftM (Lean.Meta.inferType brecOn) let cls : Lean.Name := `Elab.definition.structural let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Structural.M Lean.Expr := fun y => let cls := `Elab.definition.structural; do let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Structural.M Lean.Expr := fun y => Lean.Meta.forallBoundedTelescope brecOnType (some 1) fun F x => let F := Array.getOp F 0; do let FType ← liftM (Lean.Meta.inferType F) let cls : Lean.Name := `Elab.definition.structural let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.Structural.M Lean.Expr := fun y => do let FType ← liftM (Lean.Meta.instantiateForall FType recArgInfo.indIndices) let FType ← liftM (Lean.Meta.instantiateForall FType #[major]) Lean.Meta.forallBoundedTelescope FType (some 1) fun below x => let below := Array.getOp below 0; do let valueNew ← Lean.Elab.Structural.replaceRecApps recFnName recArgInfo below value let Farg ← liftM (Lean.Meta.mkLambdaFVars (recArgInfo.indIndices ++ #[major, below] ++ otherArgs) valueNew false true) let brecOn : Lean.Expr := Lean.mkApp brecOn Farg pure (Lean.mkAppN brecOn otherArgs) if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "FType: " ++ Lean.toMessageData FType ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "brecOnType " ++ Lean.toMessageData brecOnType ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "brecOn " ++ Lean.toMessageData brecOn ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "brecOn motive: " ++ Lean.toMessageData motive ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y; if (recArgInfo.reflexive && brecOnUniv != Lean.levelZero) = true then do let r ← liftM (Lean.Meta.decLevel brecOnUniv) let brecOnUniv : Lean.Level := r let y ← pure PUnit.unit _do_jp brecOnUniv y else do let y ← pure PUnit.unit _do_jp brecOnUniv y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "brecOn univ: " ++ Lean.toMessageData brecOnUniv ++ Lean.toMessageData "") _do_jp brecOnUniv y else do let y ← pure PUnit.unit _do_jp brecOnUniv y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "fixedParams: " ++ Lean.toMessageData recArgInfo.fixedParams ++ Lean.toMessageData ", otherArgs: " ++ Lean.toMessageData otherArgs ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "mkBRecOn: " ++ Lean.toMessageData value ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y