def Lean.Parser.Tactic.anchor : ParserDescr

Equations

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

def Lean.Parser.Tactic.grindLemma : ParserDescr

Equations

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

def Lean.Parser.Tactic.grindLemmaMin : ParserDescr

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

Equations

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

def Lean.Parser.Tactic.grindErase : ParserDescr

Equations

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

def Lean.Parser.Tactic.grindParam : ParserDescr

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

Equations

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

def Lean.Parser.Category.grind_filter : Category

Equations

• Lean.Parser.Category.grind_filter = { }

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

Equations

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

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

Equations

• Lean.Parser.Tactic.Grind.grind_filter_ = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.grind_filter_ 1024 (Lean.ParserDescr.const `ident)

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

• Lean.Parser.Category.grind = { }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

skip does nothing.

Equations

• Lean.Parser.Tactic.Grind.skip = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.skip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)

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

lia linear integer arithmetic.

Equations

• Lean.Parser.Tactic.Grind.lia = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.lia 1024 (Lean.ParserDescr.nonReservedSymbol "lia" false)

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

ring (commutative) rings and fields.

Equations

• Lean.Parser.Tactic.Grind.ring = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.ring 1024 (Lean.ParserDescr.nonReservedSymbol "ring" false)

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

ac associativity and commutativity procedure.

Equations

• Lean.Parser.Tactic.Grind.ac = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.ac 1024 (Lean.ParserDescr.nonReservedSymbol "ac" false)

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

linarith linear arithmetic.

Equations

• Lean.Parser.Tactic.Grind.linarith = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.linarith 1024 (Lean.ParserDescr.nonReservedSymbol "linarith" false)

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

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

Equations

• Lean.Parser.Tactic.Grind.sorry = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.sorry 1024 (Lean.ParserDescr.nonReservedSymbol "sorry" false)

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

Equations

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

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.

Equations

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

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

Shorthand for instantiate only

Equations

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

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

Shows asserted facts.

Equations

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

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

Shows propositions known to be True.

Equations

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

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

Shows propositions known to be False.

Equations

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

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

Shows equivalence classes of terms.

Equations

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

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

Show case-split candidates.

Equations

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

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

Show grind state.

Equations

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

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

Show active local theorems and their anchors for heuristic instantiation.

Equations

• Lean.Parser.Tactic.Grind.showLocalThms = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.showLocalThms 1024 (Lean.ParserDescr.nonReservedSymbol "show_local_thms" false)

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

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

Equations

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

def Lean.Parser.Category.grind_ref : Category

Equations

• Lean.Parser.Category.grind_ref = { }

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

Equations

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

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

Equations

• Lean.Parser.Tactic.Grind.grind_ref_ = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.grind_ref_ 1024 Lean.Parser.Tactic.anchor

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

Equations

• Lean.Parser.Tactic.Grind.grind_ref__1 = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.grind_ref__1 1022 (Lean.ParserDescr.cat `term 0)

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.

Equations

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

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.

Equations

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

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

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

Equations

• Lean.Parser.Tactic.Grind.casesNext = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.casesNext 1024 (Lean.ParserDescr.nonReservedSymbol "cases_next" false)

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

done succeeds iff there are no remaining goals.

Equations

• Lean.Parser.Tactic.Grind.done = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.done 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)

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

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

Equations

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

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

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

Equations

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

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.

Equations

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

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

Executes the given tactic block to close the current goal.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

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'.

Equations

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

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

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

Equations

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

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

try tac runs tac and succeeds even if tac failed.

Equations

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

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

fail_if_success t fails if the tactic t succeeds.

Equations

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

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

admit is a synonym for sorry.

Equations

• Lean.Parser.Tactic.Grind.grindAdmit = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.grindAdmit 1024 (Lean.ParserDescr.nonReservedSymbol "admit" false)

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

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

Equations

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

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.

Equations

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

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

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

Equations

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

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.

Equations

• Lean.Parser.Tactic.Grind.exposeNames = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.exposeNames 1024 (Lean.ParserDescr.nonReservedSymbol "expose_names" false)

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.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• Lean.Parser.Tactic.Grind.mbtc = Lean.ParserDescr.node `Lean.Parser.Tactic.Grind.mbtc 1024 (Lean.ParserDescr.nonReservedSymbol "mbtc" false)