Documentation

Equations

• Lean.Elab.Tactic.evalGeneralize stx = Lean.Elab.Tactic.withMainContext do let args ← Array.mapM (fun arg => let hName? := if Lean.Syntax.isNone (Lean.Syntax.getOp arg 0) = true then none else some (Lean.Syntax.getId (Lean.Syntax.getOp (Lean.Syntax.getOp arg 0) 0)); do let expr ← Lean.Elab.Tactic.elabTerm (Lean.Syntax.getOp arg 1) none false pure { expr := expr, xName? := some (Lean.Syntax.getId (Lean.Syntax.getOp arg 3)), hName? := hName? }) (Lean.Syntax.getSepArgs (Lean.Syntax.getOp stx 1)) Lean.Elab.Tactic.liftMetaTactic fun mvarId => do let discr ← Lean.Meta.generalize mvarId args let x : Array Lean.FVarId × Lean.MVarId := discr match x with | (x, mvarId) => pure [mvarId]