Equations
- Lean.Meta.instInhabitedGeneralizeArg = { default := { expr := default, xName? := default, hName? := default } }
Equations
- Lean.Meta.generalize mvarId args = Lean.Meta.withMVarContext mvarId do Lean.Meta.checkNotAssigned mvarId `generalize let tag ← Lean.Meta.getMVarTag mvarId let a ← Lean.Meta.getMVarType mvarId let target ← Lean.Meta.instantiateMVars a (fun go => do let targetNew ← go 0 let a ← Lean.Meta.isTypeCorrect targetNew let _do_jp : PUnit → Lean.MetaM (Array Lean.FVarId × Lean.MVarId) := fun y => let es := Array.map (fun a => a.expr) args; if (!Array.any args (fun arg => Option.isSome arg.hName?) 0 (Array.size args)) = true then do let mvarNew ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar targetNew tag Lean.Meta.assignExprMVar mvarId (Lean.mkAppN mvarNew es) Lean.Meta.introNP (Lean.Expr.mvarId! mvarNew) (Array.size args) else do let discr ← Lean.Meta.forallBoundedTelescope targetNew (some (Array.size args)) fun xs type => (fun go' => do let discr ← go' 0 let x : List Lean.Expr × Lean.Expr := discr match x with | (rfls, type) => do let a ← Lean.Meta.mkForallFVars xs type false true pure (rfls, a)) (Lean.Meta.generalize.go' args xs type) let x : List Lean.Expr × Lean.Expr := discr match x with | (rfls, targetNew) => do let mvarNew ← Lean.Meta.mkFreshExprSyntheticOpaqueMVar targetNew tag Lean.Meta.assignExprMVar mvarId (Lean.mkAppN (Lean.mkAppN mvarNew es) (List.toArray rfls)) Lean.Meta.introNP (Lean.Expr.mvarId! mvarNew) (Array.size args + List.length rfls) if a = true then do let y ← pure PUnit.unit _do_jp y else do let y ← Lean.Meta.throwTacticEx `generalize mvarId (Lean.toMessageData "result is not type correct" ++ Lean.toMessageData (Lean.indentExpr targetNew) ++ Lean.toMessageData "") Lean.Syntax.missing _do_jp y) (Lean.Meta.generalize.go args target)
partial def
Lean.Meta.generalize.go
(args : Array Lean.Meta.GeneralizeArg)
(target : Lean.Expr)
(i : Nat)
:
partial def
Lean.Meta.generalize.go'
(args : Array Lean.Meta.GeneralizeArg)
(xs : Array Lean.Expr)
(type : Lean.Expr)
(i : Nat)
: