def Lean.Parser.Tactic.anchor : ParserDescr

def Lean.Parser.Tactic.grindLemma : ParserDescr

def Lean.Parser.Tactic.grindLemmaMin : ParserDescr

The ! modifier instructs grind to consider only minimal indexable subexpressions when selecting patterns.

def Lean.Parser.Tactic.grindErase : ParserDescr

def Lean.Parser.Tactic.grindParam : ParserDescr

The ! modifier instructs grind to consider only minimal indexable subexpressions when selecting patterns.

def Lean.Parser.Category.grind_filter : Category

def Lean.Parser.Tactic.Grind.grind_filter.quot : ParserDescr

def Lean.Parser.Tactic.Grind.grind_filter_ : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen<_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen!=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen≤_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen<=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen>_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen≥_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filterGen>=_» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filter(_)» : ParserDescr

def Lean.Parser.Tactic.Grind.«grind_filter_&&_» : TrailingParserDescr

def Lean.Parser.Tactic.Grind.«grind_filter_||_» : TrailingParserDescr

def Lean.Parser.Tactic.Grind.grind_filter!_ : ParserDescr

def Lean.Parser.Tactic.Grind.grindFilter : ParserDescr

def Lean.Parser.Tactic.Grind.grind.quot : ParserDescr

def Lean.Parser.Category.grind : Category

grind is the syntax category for a "grind interactive tactic". A grind tactic is a program which receives a grind goal.

def Lean.Parser.Tactic.Grind.grindStep : ParserDescr

def Lean.Parser.Tactic.Grind.grindSeq1Indented : ParserDescr

def Lean.Parser.Tactic.Grind.grindSeqBracketed : ParserDescr

def Lean.Parser.Tactic.Grind.grindSeq : ParserDescr

def Lean.Parser.Tactic.Grind.paren : ParserDescr

(grindSeq) runs the grindSeq in sequence on the current list of targets. This is pure grouping with no added effects.

def Lean.Parser.Tactic.Grind.skip : ParserDescr

skip does nothing.

def Lean.Parser.Tactic.Grind.lia : ParserDescr

lia linear integer arithmetic.

def Lean.Parser.Tactic.Grind.ring : ParserDescr

ring (commutative) rings and fields.

def Lean.Parser.Tactic.Grind.ac : ParserDescr

ac associativity and commutativity procedure.

def Lean.Parser.Tactic.Grind.linarith : ParserDescr

linarith linear arithmetic.

def Lean.Parser.Tactic.Grind.sorry : ParserDescr

The sorry tactic is a temporary placeholder for an incomplete tactic proof.

def Lean.Parser.Tactic.Grind.thmNs : ParserDescr

def Lean.Parser.Tactic.Grind.thm : ParserDescr

def Lean.Parser.Tactic.Grind.instantiate : ParserDescr

Instantiates theorems using E-matching. The approx modifier is just a marker for users to easily identify automatically generated instantiate tactics that may have redundant arguments.

def Lean.Parser.Tactic.Grind.use : ParserDescr

Shorthand for instantiate only

def Lean.Parser.Tactic.Grind.showAsserted : ParserDescr

Shows asserted facts.

def Lean.Parser.Tactic.Grind.showTrue : ParserDescr

Shows propositions known to be True.

def Lean.Parser.Tactic.Grind.showFalse : ParserDescr

Shows propositions known to be False.

def Lean.Parser.Tactic.Grind.showEqcs : ParserDescr

Shows equivalence classes of terms.

def Lean.Parser.Tactic.Grind.showCases : ParserDescr

Show case-split candidates.

def Lean.Parser.Tactic.Grind.showState : ParserDescr

Show grind state.

def Lean.Parser.Tactic.Grind.showLocalThms : ParserDescr

Show active local theorems and their anchors for heuristic instantiation.

def Lean.Parser.Tactic.Grind.showTerm : ParserDescr

show_term tac runs tac, then displays the generated proof in the InfoView.

def Lean.Parser.Tactic.Grind.grind_ref.quot : ParserDescr

def Lean.Parser.Category.grind_ref : Category

def Lean.Parser.Tactic.Grind.grind_ref_ : ParserDescr

def Lean.Parser.Tactic.Grind.grind_ref__1 : ParserDescr

def Lean.Parser.Tactic.Grind.cases : ParserDescr

Performs a case-split on a logical connective, match-expression, if-then-else-expression, or inductive predicate. The argument is an anchor referencing one of the case-split candidates in the grind state. You can use cases? to select a specific candidate using a code action.

def Lean.Parser.Tactic.Grind.casesTrace : ParserDescr

A variant of cases that provides a code-action for selecting one of the candidate case-splits available in the grind state.

def Lean.Parser.Tactic.Grind.casesNext : ParserDescr

Performs the next case-split. The case-split is selected using the same heuristic used by finish.

def Lean.Parser.Tactic.Grind.done : ParserDescr

done succeeds iff there are no remaining goals.

def Lean.Parser.Tactic.Grind.finish : ParserDescr

finish tries to close the current goal using grind's default strategy

def Lean.Parser.Tactic.Grind.finishTrace : ParserDescr

finish? tries to close the current goal using grind's default strategy and suggests a tactic script.

def Lean.Parser.Tactic.Grind.have : ParserDescr

The have tactic is for adding opaque definitions and hypotheses to the local context of the main goal. The definitions forget their associated value and cannot be unfolded.

• have h : t := e adds the hypothesis h : t if e is a term of type t.
• have h := e uses the type of e for t.
• have : t := e and have := e use this for the name of the hypothesis.

def Lean.Parser.Tactic.Grind.nestedTacticCore : ParserDescr

Executes the given tactic block to close the current goal.

def Lean.Parser.Tactic.Grind.allGoals : ParserDescr

all_goals tac runs tac on each goal, concatenating the resulting goals. If the tactic fails on any goal, the entire all_goals tactic fails.

def Lean.Parser.Tactic.Grind.focus : ParserDescr

focus tac focuses on the main goal, suppressing all other goals, and runs tac on it. Usually · tac, which enforces that the goal is closed by tac, should be preferred.

def Lean.Parser.Tactic.Grind.next : ParserDescr

next => tac focuses on the next goal and solves it using tac, or else fails. next x₁ ... xₙ => tac additionally renames the n most recent hypotheses with inaccessible names to the given names.

def Lean.Parser.Tactic.Grind.«grind·._» : ParserDescr

· grindSeq focuses on the main grind goal and tries to solve it using the given sequence of grind tactics.

def Lean.Parser.Tactic.Grind.anyGoals : ParserDescr

any_goals tac applies the tactic tac to every goal, concatenating the resulting goals for successful tactic applications. If the tactic fails on all of the goals, the entire any_goals tactic fails.

This tactic is like all_goals try tac except that it fails if none of the applications of tac succeeds.

def Lean.Parser.Tactic.Grind.withAnnotateState : ParserDescr

with_annotate_state stx t annotates the lexical range of stx : Syntax with the initial and final state of running tactic t.

def Lean.Parser.Tactic.Grind.«grind_<;>_» : TrailingParserDescr

tac <;> tac' runs tac on the main goal and tac' on each produced goal, concatenating all goals produced by tac'.

def Lean.Parser.Tactic.Grind.first : ParserDescr

first | tac | ... runs each tac until one succeeds, or else fails.

def Lean.Parser.Tactic.Grind.grindTry_ : ParserDescr

try tac runs tac and succeeds even if tac failed.

def Lean.Parser.Tactic.Grind.failIfSuccess : ParserDescr

fail_if_success t fails if the tactic t succeeds.

def Lean.Parser.Tactic.Grind.grindAdmit : ParserDescr

admit is a synonym for sorry.

def Lean.Parser.Tactic.Grind.fail : ParserDescr

fail msg is a tactic that always fails, and produces an error using the given message.

def Lean.Parser.Tactic.Grind.grindRepeat_ : ParserDescr

repeat tac repeatedly applies tac so long as it succeeds. The tactic tac may be a tactic sequence, and if tac fails at any point in its execution, repeat will revert any partial changes that tac made to the tactic state. The tactic tac should eventually fail, otherwise repeat tac will run indefinitely.

def Lean.Parser.Tactic.Grind.renameI : ParserDescr

rename_i x_1 ... x_n renames the last n inaccessible names using the given names.

def Lean.Parser.Tactic.Grind.exposeNames : ParserDescr

expose_names renames all inaccessible variables with accessible names, making them available for reference in generated tactics. However, this renaming introduces machine-generated names that are not fully under user control. expose_names is primarily intended as a preamble for generated grind tactic scripts.

def Lean.Parser.Tactic.Grind.setOption : ParserDescr

set_option opt val in tacs (the tactic) acts like set_option opt val at the command level, but it sets the option only within the tactics tacs.

def Lean.Parser.Tactic.Grind.setConfig : ParserDescr

set_config configItem+ in tacs executes tacs with the updated configuration options configItem+

def Lean.Parser.Tactic.Grind.haveSilent : ParserDescr

Proves <term> using the current grind state and default search strategy.

def Lean.Parser.Tactic.Grind.mbtc : ParserDescr

Adds new case-splits using model-based theory combination.