def
Lean.Elab.Structural.mkIndPredBRecOn
(recFnName : Lean.Name)
(recArgInfo : Lean.Elab.Structural.RecArgInfo)
(value : Lean.Expr)
:
Equations
- Lean.Elab.Structural.mkIndPredBRecOn recFnName recArgInfo value = 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 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 := Lean.mkConst (Lean.mkBRecOnName recArgInfo.indName) 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 => do let FType ← 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) liftM (Lean.Meta.instantiateForall FType #[major]) 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 Lean.Meta.forallBoundedTelescope FType (some 1) fun below x => do let _ ← liftM (Lean.Meta.mkFreshExprSyntheticOpaqueMVar FType Lean.Name.anonymous) let below : Lean.Expr := Array.getOp below 0 let valueNew ← Lean.Elab.Structural.replaceIndPredRecApps recFnName recArgInfo motive 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 "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 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