Extensions to the case tactic

Adds a variant of case that looks for a goal with a particular type, rather than a goal with a particular tag. For consistency with case, it takes a tag as well, but the tag can be a hole _.

Also adds case' extensions.

def Std.Tactic.casePattArg : Lean.ParserDescr

Clause for a case ... : ... tactic.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.casePattTac : Lean.ParserDescr

The body of a case ... | ... tactic that's a tactic sequence (or hole).

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.casePattExpr : Lean.ParserDescr

The body of a case ... | ... tactic that's an exact term.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.casePattBody : Lean.ParserDescr

The body of a case ... : ... tactic.

Equations

• Std.Tactic.casePattBody = Lean.ParserDescr.nodeWithAntiquot "casePattBody" `Std.Tactic.casePattBody (Lean.ParserDescr.binary `orelse Std.Tactic.casePattTac Std.Tactic.casePattExpr)

def Std.Tactic.casePatt : Lean.ParserDescr

• case _ : t => tac finds the first goal that unifies with t and then solves it using tac or else fails. Like show, it changes the type of the goal to t. The _ can optionally be a case tag, in which case it only looks at goals whose tag would be considered by case (goals with an exact tag match, followed by goals with the tag as a suffix, followed by goals with the tag as a prefix).

• case _ n₁ ... nₘ : t => tac additionally names the m most recent hypotheses with inaccessible names to the given names. The names are renamed before matching against t. The _ can optionally be a case tag.

• case _ : t := e is short for case _ : t => exact e.

• case _ : t₁ | _ : t₂ | ... => tac is equivalent to (case _ : t₁ => tac); (case _ : t₂ => tac); ... but with all matching done on the original list of goals -- each goal is consumed as they are matched, so patterns may repeat or overlap.

• case _ : t will make the matched goal be the first goal. case _ : t₁ | _ : t₂ | ... makes the matched goals be the first goals in the given order.

• case _ : t := _ and case _ : t := ?m are the same as case _ : t but in the ?m case the goal tag is changed to m. In particular, the goal becomes metavariable ?m.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.casePatt' : Lean.ParserDescr

case' _ : t => tac is similar to the case _ : t => tac tactic, but it does not ensure the goal has been solved after applying tac, nor does it admit the goal if tac failed. Recall that case closes the goal using sorry when tac fails, and the tactic execution is not interrupted.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.findGoalOfPatt (gs : List Lean.MVarId) (tag : Lean.TSyntax `Lean.binderIdent) (patt? : Option Lean.Term) (renameI : Lean.TSyntaxArray `Lean.binderIdent) : Lean.Elab.Tactic.TacticM (Lean.MVarId × List Lean.MVarId × List Lean.MVarId)

Find the first goal among those matching tag whose type unifies with patt. The renameI array consists of names to use to rename inaccessibles. The patt term is elaborated in the context where the inaccessibles have been renamed.

Returns the found goal, goals caused by elaborating patt, and the remaining goals.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.processCasePattBody (stx : Lean.TSyntax `Std.Tactic.casePattTac) : Lean.Elab.Tactic.TacticM (Lean.Term ⊕ Lean.Syntax × Lean.TSyntax `Lean.Parser.Tactic.tacticSeq)

Given a casePattBody, either give a synthetic hole or a tactic sequence (along with the syntax for the =>). Converts holes into synthetic holes since they are processed with elabTermWithHoles.

Equations

• One or more equations did not get rendered due to their size.

def Std.Tactic.evalCase (close : Bool) (stx : Lean.Syntax) (tags : Array (Lean.TSyntax `Lean.binderIdent)) (hss : Array (Lean.TSyntaxArray `Lean.binderIdent)) (patts? : Array (Option Lean.Term)) (caseBody : Lean.TSyntax `Std.Tactic.casePattTac) : Lean.Elab.Tactic.TacticM Unit

Implementation for case and case'.

Equations

• One or more equations did not get rendered due to their size.