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.thmNs : ParserDescr

Equations

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

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.Tactic.Grind.showGoals : ParserDescr

Shows the pending goals.

Equations

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

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__/__» : ParserDescr

Anchor with an ordinal disambiguator. Distinct case-split candidates may have the same anchor. For example, two candidates that differ only in inaccessible variables have identical anchors. #a56e/2 refers to the second candidate (in the case-split candidate list) matching the anchor #a56e.

Equations

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

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. If multiple candidates match the anchor (e.g., they differ only in inaccessible variables), an ordinal reference such as #a56e/2 selects the second matching candidate.

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)

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

intro x₁ ... xₙ introduces binders and internalizes them into the E-graph. Only available in sym => mode. intro with no arguments introduces one binder with an inaccessible name. Use intro (internalize := false) or intro~ to skip internalization.

Equations

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

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

intro~ x₁ ... xₙ is shorthand for intro (internalize := false).

Equations

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

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

intros introduces all remaining binders and internalizes them. Only available in sym => mode. Use intros (internalize := false) or intros~ to skip internalization.

Equations

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

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

intros~ is shorthand for intros (internalize := false).

Equations

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

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

apply t applies theorem t as a backward rule. Only available in sym => mode. When used with repeat, the backward rule is cached for efficiency.

Equations

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

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

internalize internalizes hypotheses into the grind E-graph. Only available in sym => mode.

• internalize internalizes the next hypothesis.
• internalize <num> internalizes the next <num> hypotheses.

Equations

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

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

internalize_all internalizes all pending hypotheses into the grind E-graph. Only available in sym => mode.

Equations

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

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

by_contra applies proof by contradiction, negating the target and making it False. Only available in sym => mode.

Equations

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

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

simp applies the structural simplifier to the goal target. Only available in sym => mode.

• simp — uses the default (identity) variant
• simp myVariant — uses a named variant registered via register_sym_simp
• simp [thm₁, thm₂, ...] — default variant with extra rewrite theorems appended to post
• simp myVariant [thm₁, thm₂, ...] — named variant with extra theorems

Equations

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

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

dsimp applies the definitional simplifier to the goal target. Only available in sym => mode.

• dsimp — uses the default (identity) variant
• dsimp myVariant — uses a named variant registered via register_sym_dsimp
• dsimp [id₁, id₂, ...] — default variant with extra declarations to unfold
• dsimp myVariant [id₁, id₂, ...] — named variant with extra declarations

Equations

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

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

exact e closes the main goal if its target type matches that of e.

Equations

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

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

cbv performs simplification that closely mimics call-by-value evaluation. It reduces terms by unfolding definitions using their defining equations and applying matcher equations. The unfolding is propositional, so cbv also works with functions defined via well-founded recursion or partial fixpoints.

cbv reduces the goal target using call-by-value evaluation. For equation goals (lhs = rhs), cbv automatically attempts refl after reduction to close the goal.

Unlike the standalone cbv tactic, this variant does not support the at location syntax: in sym => mode it only reduces the goal target.

cbv is not a finishing tactic in general: it may leave a new (simpler) goal.

The proofs produced by cbv only use the three standard axioms. In particular, they do not require trust in the correctness of the code generator.

This is a variant of cbv that only works in sym => mode.

Equations

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