def Lean.Meta.Grind.congrPlaceholderProof : Expr

We use this auxiliary constant to mark delayed congruence proofs.

def Lean.Meta.Grind.eqCongrSymmPlaceholderProof : Expr

We use this auxiliary constant to mark delayed symmetric congruence proofs. Example: a = b is symmetrically congruent to c = d if a = d and b = c.

Note: We previously used congrPlaceholderProof for this case, but it caused non-termination during proof term construction when a = b = c = d. The issue was that we did not have enough information to determine how a = b and c = d became congruent. The new marker resolves this issue.

If congrPlaceholderProof is used, then a = b became congruent to c = d because a = c and b = d. If eqCongrSymmPlaceholderProof is used, then it was because a = d and b = c.

Example: suppose we have the following equivalence class:

{p, q, p = q, q = p, True}

Recall that True is always the root of its equivalence class. Assume we also have the following two paths in the class:

1. p -> p = q -> q = p -> True
2. q -> True

Now suppose we try to build a proof for p = True. We must construct a proof for (p = q) = (q = p). These equalities are congruent, but if we try to prove p = q and q = p using the facts p = True and q = True, we end up trying to prove p = True again. In other words, we are missing the information that p = q became congruent to q = p because of the symmetric case. By using eqCongrSymmPlaceholderProof, we retain this information.

def Lean.Meta.Grind.isInterpreted (e : Expr) : MetaM Bool

Returns true if e is True, False, or a literal value. See Lean.Meta.LitValues for supported literals.

opaque Lean.Meta.Grind.grind.debug : Lean.Option Bool

opaque Lean.Meta.Grind.grind.debug.proofs : Lean.Option Bool

opaque Lean.Meta.Grind.grind.warning : Lean.Option Bool

structure Lean.Meta.Grind.AnchorRef : Type

Anchors are used to reference terms, local theorems, and case-splits in the grind state. We also use anchors to prune the search space when they are provided as grind parameters and the finish tactic.

• numDigits : Nat
• anchorPrefix : UInt64

opaque Lean.Meta.Grind.SolverExtensionStateSpec : (α : Type) × Inhabited α

Opaque solver extension state.

def Lean.Meta.Grind.SolverExtensionState : Type

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSolverExtensionState : Inhabited SolverExtensionState

inductive Lean.Meta.Grind.SplitSource : Type

Case-split source. That is, where it came from. We store the current source in the grind context.

• ematch (origin : Origin) : SplitSource

  Generated while instantiating a theorem using E-matching.

• ext (declName : Name) : SplitSource

  Generated while instantiating an extensionality theorem with name declName

• mbtc (a b : Expr) (i : Nat) : SplitSource

  Model-based theory combination equality coming from the i-th argument of applications a and b

• beta (e : Expr) : SplitSource

  Beta-reduction.

• forallProp (e : Expr) : SplitSource

  Forall-propagator.

• existsProp (e : Expr) : SplitSource

  Exists-propagator.

• input : SplitSource

  Input goal

• inj (origin : Origin) : SplitSource

  Injectivity theorem.

• guard (origin : Origin) : SplitSource

  grind_pattern guard

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSplitSource : Inhabited SplitSource

def Lean.Meta.Grind.instInhabitedSplitSource.default : SplitSource

def Lean.Meta.Grind.SplitSource.toMessageData : SplitSource → MessageData

structure Lean.Meta.Grind.Context : Type

Context for GrindM monad.

• simp : Simp.Context
• simpMethods : Simp.Methods
• config : Grind.Config
• anchorRefs? : Option (Array AnchorRef)

  If anchorRefs? := some anchorRefs, then only local instances and case-splits in anchorRefs are considered.

• cheapCases : Bool

  If cheapCases is true, grind only applies cases to types that contain at most one minor premise. Recall that grind applies cases when introducing types tagged with [grind cases eager], and at Split.lean Remark: We add this option to implement the lookahead feature, we don't want to create several subgoals when performing lookahead.

• reportMVarIssue : Bool
• splitSource : SplitSource

  Current source of case-splits.

• symPrios : SymbolPriorities

  Symbol priorities for inferring E-matching patterns

• extensions : ExtensionStateArray
• debug : Bool

structure Lean.Meta.Grind.CongrTheoremCacheKey : Type

Key for the congruence theorem cache.

• f : Expr
• numArgs : Nat

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqCongrTheoremCacheKey : BEq CongrTheoremCacheKey

@[implicit_reducible]

instance Lean.Meta.Grind.instHashableCongrTheoremCacheKey : Hashable CongrTheoremCacheKey

structure Lean.Meta.Grind.Counters : Type

• thm : PHashMap Origin Nat

  Number of times E-match theorem has been instantiated.

• case : PHashMap Name Nat

  Number of times a cases has been performed on an inductive type/predicate

• apps : PHashMap Name Nat

  Number of applications per function symbol. This information is only collected if set_option diagnostics true

def Lean.Meta.Grind.instInhabitedCounters.default : Counters

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedCounters : Inhabited Counters

structure Lean.Meta.Grind.SplitDiagInfo : Type

Case-split diagnostic information

• lctx : LocalContext
• c : Expr
• gen : Nat
• numCases : Nat
• splitSource : SplitSource

structure Lean.Meta.Grind.State : Type

State for the GrindM monad.

• congrThms : PHashMap CongrTheoremCacheKey CongrTheorem

  Congruence theorems generated so far. Recall that for constant symbols we rely on the reserved name feature (i.e., mkHCongrWithArityForConst?). Remark: we currently do not reuse congruence theorems

• simp : Simp.State
• lastTag : Name

  Used to generate trace messages of the for [grind] working on <tag>, and implement the macro trace_goal.

• issues : List MessageData

  Issues found during the proof search. These issues are reported to users when grind fails.

• counters : Counters

  Performance counters

• splitDiags : PArray SplitDiagInfo

  Split diagnostic information. This information is only collected when set_option diagnostics true

• lawfulEqCmpMap : PHashMap ExprPtr (Option Expr)

  Mapping from binary functions f to a theorem thm : ∀ a b, f a b = .eq → a = b if it implements the LawfulEqCmp type class.

• reflCmpMap : PHashMap ExprPtr (Option Expr)

  Mapping from binary functions f to a theorem thm : ∀ a, f a a = .eq if it implements the ReflCmp type class.

• anchors : PHashMap ExprPtr UInt64

  Cached anchors (aka stable hash codes) for terms in the grind state.

instance Lean.Meta.Grind.instNonemptyState : Nonempty State

def Lean.Meta.Grind.MethodsRef : Type

instance Lean.Meta.Grind.instNonemptyMethodsRef : Nonempty MethodsRef

@[reducible, inline]

abbrev Lean.Meta.Grind.GrindM (α : Type) : Type

@[inline]

def Lean.Meta.Grind.mapGrindM {m : Type → Type u_1} [MonadControlT GrindM m] [Monad m] (f : {α : Type} → GrindM α → GrindM α) {α : Type} (x : m α) : m α

@[inline]

def Lean.Meta.Grind.isDebugEnabled : GrindM Bool

Returns true if grind.debug is set

structure Lean.Meta.Grind.SavedState : Type

Backtrackable state for the GrindM monad.

• meta : Meta.SavedState
• grind : State

instance Lean.Meta.Grind.instNonemptySavedState : Nonempty SavedState

def Lean.Meta.Grind.saveState : GrindM SavedState

def Lean.Meta.Grind.SavedState.restore (b : SavedState) : GrindM Unit

Restore backtrackable parts of the state.

@[implicit_reducible]

instance Lean.Meta.Grind.instMonadBacktrackSavedStateGrindM : MonadBacktrack SavedState GrindM

def Lean.Meta.Grind.withoutReportingMVarIssues {m : Type → Type u_1} {α : Type} [MonadControlT GrindM m] [Monad m] : m α → m α

withoutReportingMVarIssues x executes x without reporting metavariables found during internalization. See comment at Grind.Context.reportMVarIssue for additional details.

def Lean.Meta.Grind.withSplitSource {m : Type → Type u_1} {α : Type} [MonadControlT GrindM m] [Monad m] (splitSource : SplitSource) : m α → m α

withSplitSource s x executes x and uses s as the split source for any case-split registered.

def Lean.Meta.Grind.getConfig : GrindM Grind.Config

Returns the user-defined configuration options

def Lean.Meta.Grind.getExtensions : GrindM ExtensionStateArray

Returns extension states associate with grind attributes in use

@[reducible, inline]

abbrev Lean.Meta.Grind.withGTransparency {n : Type → Type u_1} {α : Type} [MonadControlT MetaM n] [MonadLiftT GrindM n] [Monad n] (k : n α) : n α

Runs k with the transparency setting specified by Config.reducible. Uses reducible transparency if reducible is true, otherwise default transparency.

def Lean.Meta.Grind.getAnchorRefs : GrindM (Option (Array AnchorRef))

Returns the anchor references (if any) being used to restrict the search.

def Lean.Meta.Grind.resetAnchors : GrindM Unit

def Lean.Meta.Grind.cheapCasesOnly : GrindM Bool

def Lean.Meta.Grind.withCheapCasesOnly {α : Type} (k : GrindM α) : GrindM α

def Lean.Meta.Grind.reportMVarInternalization : GrindM Bool

def Lean.Meta.Grind.getSymbolPriorities : GrindM SymbolPriorities

Returns symbol priorities for inferring E-matching patterns.

def Lean.Meta.Grind.hasFunCCModifier (declName : Name) : GrindM Bool

Returns true if we declName is tagged with funCC modifier.

def Lean.Meta.Grind.isSplit (declName : Name) : GrindM Bool

def Lean.Meta.Grind.isEagerSplit (declName : Name) : GrindM Bool

def Lean.Meta.Grind.isExtTheorem (declName : Name) : GrindM Bool

def Lean.Meta.Grind.isMatchEqLikeDeclName (declName : Name) : CoreM Bool

Returns true if declName is the name of a match equation or a match congruence equation.

def Lean.Meta.Grind.getEMatchTheoremNumInstances (thm : EMatchTheorem) : GrindM Nat

def Lean.Meta.Grind.saveCases (declName : Name) : GrindM Unit

def Lean.Meta.Grind.saveAppOf (h : HeadIndex) : GrindM Unit

def Lean.Meta.Grind.saveSplitDiagInfo (c : Expr) (gen numCases : Nat) (splitSource : SplitSource) : GrindM Unit

@[inline]

def Lean.Meta.Grind.getMethodsRef : GrindM MethodsRef

def Lean.Meta.Grind.getMaxGeneration : GrindM Nat

Returns maximum term generation that is considered during ematching.

def Lean.Meta.Grind.abstractNestedProofs (e : Expr) : GrindM Expr

Abstracts nested proofs in e. This is a preprocessing step performed before internalization.

def Lean.Meta.Grind.mkHCongrWithArity (f : Expr) (numArgs : Nat) : GrindM CongrTheorem

Creates a congruence theorem for a f-applications with numArgs arguments.

def Lean.Meta.Grind.reportIssue (msg : MessageData) : GrindM Unit

def Lean.Meta.Grind.doElemReportIssue!__ : ParserDescr

def Lean.Meta.Grind.expandReportDbgIssueMacro (s : Syntax) : MacroM (TSyntax `doElem)

Similar to expandReportIssueMacro, but only reports issue if grind.debug is set to true

def Lean.Meta.Grind.doElemReportDbgIssue!__ : ParserDescr

Similar to reportIssue!, but only reports issue if grind.debug is set to true

inductive Lean.Meta.Grind.SolverTerms : Type

Each E-node may have "solver terms" attached to them. Each term is an element of the equivalence class that the solver cares about. Each solver is responsible for marking the terms they care about. The grind core propagates equalities and disequalities to the theory solvers using these "marked" terms. The root of the equivalence class contains a list of representatives sorted by solver id. Note that many E-nodes do not have any solver terms attached to them.

"Solver terms" are referenced as "theory variables" in the SMT literature. The SMT solver Z3 uses a similar representation.

• nil : SolverTerms
• next (solverId : Nat) (e : Expr) (rest : SolverTerms) : SolverTerms

def Lean.Meta.Grind.instInhabitedSolverTerms.default : SolverTerms

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSolverTerms : Inhabited SolverTerms

def Lean.Meta.Grind.instReprSolverTerms.repr : SolverTerms → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Grind.instReprSolverTerms : Repr SolverTerms

structure Lean.Meta.Grind.ENode : Type

Stores information for a node in the E-graph. Each internalized expression e has an ENode associated with it.

• self : Expr

  Node represented by this ENode.

• next : Expr

  Next element in the equivalence class.

• root : Expr

  Root (aka canonical representative) of the equivalence class

• congr : Expr

  congr is the term self is congruent to. We say self is the congruence class root if isSameExpr congr self. This field is initialized to self even if e is not an application.

• target? : Option Expr

  When e was added to this equivalence class because of an equality h : e = target, then we store target here, and h at proof?.

• proof? : Option Expr
• flipped : Bool

  Proof has been flipped.

• size : Nat

  Number of elements in the equivalence class, this field is meaningless if node is not the root.

• interpreted : Bool

  interpreted := true if node should be viewed as an abstract value.

• ctor : Bool

  ctor := true if the head symbol is a constructor application.

• hasLambdas : Bool

  hasLambdas := true if the equivalence class contains lambda expressions.

• heqProofs : Bool

  If heqProofs := true, then some proofs in the equivalence class are based on heterogeneous equality.

• idx : Nat

  Unique index used for pretty printing and debugging purposes.

• generation : Nat

  The generation in which this enode was created.

• mt : Nat

  Modification time

• sTerms : SolverTerms

  Solver terms attached to this E-node.

• funCC : Bool

  If funCC := true, then the expression associated with this entry is an application, and function congruence closure is enabled for it. See Grind.Config.funCC for additional details.

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedENode : Inhabited ENode

def Lean.Meta.Grind.instInhabitedENode.default : ENode

def Lean.Meta.Grind.instReprENode.repr : ENode → Nat → Format

@[implicit_reducible]

instance Lean.Meta.Grind.instReprENode : Repr ENode

def Lean.Meta.Grind.ENode.isRoot (n : ENode) : Bool

def Lean.Meta.Grind.ENode.isCongrRoot (n : ENode) : Bool

inductive Lean.Meta.Grind.NewFact : Type

New equalities and facts to be processed.

• eq (lhs rhs proof : Expr) (isHEq : Bool) : NewFact
• fact (prop proof : Expr) (generation : Nat) : NewFact

def Lean.Meta.Grind.NewFact.toExpr : NewFact → MetaM Expr

def Lean.Meta.Grind.ENodeMap : Type

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedENodeMap : Inhabited ENodeMap

structure Lean.Meta.Grind.CongrKey (enodes : ENodeMap) : Type

Key for the congruence table. We need access to the enodes to be able to retrieve the equivalence class roots.

• e : Expr

@[implicit_reducible]

instance Lean.Meta.Grind.instHashableCongrKey {enodeMap : ENodeMap} : Hashable (CongrKey enodeMap)

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqCongrKey {enodeMap : ENodeMap} : BEq (CongrKey enodeMap)

@[reducible, inline]

abbrev Lean.Meta.Grind.CongrTable (enodeMap : ENodeMap) : Type

structure Lean.Meta.Grind.ParentSet : Type

• parents : List Expr

def Lean.Meta.Grind.instInhabitedParentSet.default : ParentSet

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedParentSet : Inhabited ParentSet

def Lean.Meta.Grind.ParentSet.insert (ps : ParentSet) (p : Expr) : ParentSet

def Lean.Meta.Grind.ParentSet.isEmpty (ps : ParentSet) : Bool

def Lean.Meta.Grind.ParentSet.elems (ps : ParentSet) : List Expr

@[reducible, inline]

abbrev Lean.Meta.Grind.ParentMap : Type

structure Lean.Meta.Grind.PreInstance : Type

The E-matching module instantiates theorems using the EMatchTheorem proof and a (partial) assignment. We want to avoid instantiating the same theorem with the same assignment more than once. Therefore, we store the (pre-)instance information in set. Recall that the proofs of activated theorems have been hash-consed. The assignment contains internalized expressions, which have also been hash-consed.

Note: We used to use pointer equality to implement PreInstanceSet. However, this low-level trick was incorrect in interactive mode because we add new EMatchTheorem objects using instantiate [...]. For example, suppose we write

instantiate [thm_1]; instantiate [thm_1]

The EMatchTheorem object thm_1 is created twice. Using pointer equality will miss instances created using the two different objects. Recall we do not use hash-consing on proof objects. If we hash-cons the proof objects, it would be ok to use pointer equality.

• proof : Expr
• assignment : Array Expr

@[implicit_reducible]

instance Lean.Meta.Grind.instHashablePreInstance : Hashable PreInstance

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqPreInstance : BEq PreInstance

@[reducible, inline]

abbrev Lean.Meta.Grind.PreInstanceSet : Type

structure Lean.Meta.Grind.NewRawFact : Type

New raw fact to be preprocessed, and then asserted.

• proof : Expr
• prop : Expr
• generation : Nat
• splitSource : SplitSource

  splitSource to use when internalizing this fact.

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedNewRawFact : Inhabited NewRawFact

def Lean.Meta.Grind.instInhabitedNewRawFact.default : NewRawFact

structure Lean.Meta.Grind.CanonArgKey : Type

• f : Expr
• i : Nat
• arg : Expr

def Lean.Meta.Grind.instBEqCanonArgKey.beq : CanonArgKey → CanonArgKey → Bool

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqCanonArgKey : BEq CanonArgKey

@[implicit_reducible]

instance Lean.Meta.Grind.instHashableCanonArgKey : Hashable CanonArgKey

def Lean.Meta.Grind.instHashableCanonArgKey.hash : CanonArgKey → UInt64

structure Lean.Meta.Grind.Canon.State : Type

Canonicalizer state. See Canon.lean for additional details.

• argMap : PHashMap (Expr × Nat) (List (Expr × Expr))
• canon : PHashMap Expr Expr
• proofCanon : PHashMap Expr Expr
• canonArg : PHashMap CanonArgKey Expr

@[implicit_reducible]

instance Lean.Meta.Grind.Canon.instInhabitedState : Inhabited State

def Lean.Meta.Grind.Canon.instInhabitedState.default : State

structure Lean.Meta.Grind.CaseTrace : Type

Trace information for a case split.

• expr : Expr
• i : Nat
• num : Nat
• source : SplitSource

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedCaseTrace : Inhabited CaseTrace

def Lean.Meta.Grind.instInhabitedCaseTrace.default : CaseTrace

structure Lean.Meta.Grind.TheoremGuard : Type

Users can attach guards to grind_patterns. A guard ensures that a theorem is instantiated only when the guard expression becomes provably true.

If check is true, then grind attempts to prove e by asserting its negation and checking whether this leads to a contradiction.

• e : Expr
• check : Bool

def Lean.Meta.Grind.instInhabitedTheoremGuard.default : TheoremGuard

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedTheoremGuard : Inhabited TheoremGuard

structure Lean.Meta.Grind.DelayedTheoremInstance : Type

A delayed theorem instantiation is an instantiation that includes one or more guards. See TheoremGuard.

• thm : EMatchTheorem
• proof : Expr
• prop : Expr
• generation : Nat
• guards : List TheoremGuard

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedDelayedTheoremInstance : Inhabited DelayedTheoremInstance

def Lean.Meta.Grind.instInhabitedDelayedTheoremInstance.default : DelayedTheoremInstance

structure Lean.Meta.Grind.EMatch.State : Type

E-matching related fields for the grind goal.

• thmMap : EMatchTheoremsArray

  Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols. Local theorem provided by users are added directly into newThms.

• gmt : Nat

  Goal modification time.

• thms : PArray EMatchTheorem

  Active theorems that we have performed ematching at least once.

• newThms : PArray EMatchTheorem

  Active theorems that we have not performed any round of ematching yet.

• numInstances : Nat

  Number of theorem instances generated so far.

• numDelayedInstances : Nat

  Number of delayed theorem instances generated so far. We track them to decide whether E-match made progress or not.

• num : Nat

  Number of E-matching rounds performed in this goal since the last case-split.

• preInstances : PreInstanceSet

  (pre-)instances found so far. It includes instances that failed to be instantiated.

• nextThmIdx : Nat

  Next local E-match theorem idx.

• matchEqNames : PHashSet Name

  match auxiliary functions whose equations have already been created and activated.

• delayedThmInsts : PHashMap ExprPtr (List DelayedTheoremInstance)

  Delayed instantiations is a mapping from guards to theorems that are waiting them to become True.

def Lean.Meta.Grind.EMatch.instInhabitedState.default : State

@[implicit_reducible]

instance Lean.Meta.Grind.EMatch.instInhabitedState : Inhabited State

inductive Lean.Meta.Grind.SplitInfo : Type

Case-split information.

• default (e : Expr) (source : SplitSource) : SplitInfo

  Term e may be an inductive predicate, match-expression, if-expression, implication, etc.

• imp (e : Expr) (h : e.isForall = true) (source : SplitSource) : SplitInfo

  e is an implication and we want to split on its antecedent.

• arg (a b : Expr) (i : Nat) (eq : Expr) (source : SplitSource) : SplitInfo

  Given applications a and b, case-split on whether the corresponding i-th arguments are equal or not. The split is only performed if all other arguments are already known to be equal or are also tagged as split candidates.

def Lean.Meta.Grind.instInhabitedSplitInfo.default : SplitInfo

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSplitInfo : Inhabited SplitInfo

def Lean.Meta.Grind.SplitInfo.hash : SplitInfo → UInt64

@[implicit_reducible]

instance Lean.Meta.Grind.instHashableSplitInfo : Hashable SplitInfo

def Lean.Meta.Grind.SplitInfo.beq : SplitInfo → SplitInfo → Bool

@[implicit_reducible]

instance Lean.Meta.Grind.instBEqSplitInfo : BEq SplitInfo

def Lean.Meta.Grind.SplitInfo.getExpr : SplitInfo → Expr

def Lean.Meta.Grind.SplitInfo.source : SplitInfo → SplitSource

def Lean.Meta.Grind.SplitInfo.lt : SplitInfo → SplitInfo → Bool

structure Lean.Meta.Grind.SplitArg : Type

Argument arg : type of an application app in SplitInfo.

• arg : Expr
• type : Expr
• app : Expr

structure Lean.Meta.Grind.Split.State : Type

Case splitting related fields for the grind goal.

• num : Nat

  Number of splits performed to get to this goal.

• candidates : List SplitInfo

  Case-split candidates.

• added : Std.HashSet SplitInfo

  Case-splits that have been inserted at candidates at some point.

• resolved : PHashSet ExprPtr

  Case-splits that have already been performed, or that do not have to be performed anymore.

• trace : List CaseTrace

  Sequence of cases steps that generated this goal. We only use this information for diagnostics. Remark: casesTrace.length ≥ numSplits because we don't increase the counter for cases applications that generated only 1 subgoal.

• lookaheads : List SplitInfo

  Lookahead "case-splits".

• argPosMap : Std.HashMap (Expr × Expr) (List Nat)

  A mapping (a, b) ↦ is s.t. for each SplitInfo.arg a b i eq in candidates or lookaheads we have i ∈ is. We use this information to decide whether the split/lookahead is "ready" to be tried or not.

• argsAt : PHashMap (Expr × Nat) (List SplitArg)

  Mapping from pairs (f, i) to a list of arguments. Each argument occurs as the i-th of an f-application. We use this information to add splits/lookaheads for triggering extensionality theorems and model-based theory combination. See addSplitCandidatesForExt.

@[implicit_reducible]

instance Lean.Meta.Grind.Split.instInhabitedState : Inhabited State

def Lean.Meta.Grind.Split.instInhabitedState.default : State

structure Lean.Meta.Grind.Clean.State : Type

Clean name generator.

• used : PHashSet Name
• next : PHashMap Name Nat

def Lean.Meta.Grind.Clean.instInhabitedState.default : State

@[implicit_reducible]

instance Lean.Meta.Grind.Clean.instInhabitedState : Inhabited State

structure Lean.Meta.Grind.UnitLike.State : Type

Cache for Unit-like types. It maps the type to its element. We say a type is Unit-like if it is a subsingleton and is inhabited.

• map : PHashMap ExprPtr (Option Expr)

@[implicit_reducible]

instance Lean.Meta.Grind.UnitLike.instInhabitedState : Inhabited State

def Lean.Meta.Grind.UnitLike.instInhabitedState.default : State

structure Lean.Meta.Grind.InjectiveInfo : Type

• us : List Level
• α : Expr
• β : Expr
• h : Expr
• inv? : Option (Expr × Expr)

  Inverse function and a proof that ∀ a, inv (f a) = a Note: The following two fields are none if no f-application has been found yet.

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedInjectiveInfo : Inhabited InjectiveInfo

def Lean.Meta.Grind.instInhabitedInjectiveInfo.default : InjectiveInfo

structure Lean.Meta.Grind.Injective.State : Type

State for injective theorem support.

• thms : InjectiveTheoremsArray
• fns : PHashMap ExprPtr InjectiveInfo

def Lean.Meta.Grind.Injective.instInhabitedState.default : State

@[implicit_reducible]

instance Lean.Meta.Grind.Injective.instInhabitedState : Inhabited State

structure Lean.Meta.Grind.GoalState : Type

The grind state for a goal, excluding the metavariable.

This separation from Goal allows multiple goals with different metavariables to share the same GoalState. This is useful for automation such as symbolic simulation, where applying theorems create multiple goals that inherit the same E-graph, congruence closure state, and other accumulated facts.

• nextDeclIdx : Nat

  Next local declaration index to process.

• canon : Canon.State
• enodeMap : ENodeMap
• exprs : PArray Expr
• parents : ParentMap
• congrTable : CongrTable self.enodeMap
• appMap : PHashMap HeadIndex (List Expr)

  A mapping from each function application index (HeadIndex) to a list of applications with that index. Recall that the HeadIndex for a constant is its constant name, and for a free variable, it is its unique id.

• indicesFound : PHashSet HeadIndex

  All constants (not in appMap) that have been internalized, and appMap's domain. We use this collection during theorem activation.

• newFacts : Array NewFact

  Equations and propositions to be processed.

• inconsistent : Bool

  inconsistent := true if ENodes for True and False are in the same equivalence class.

• nextIdx : Nat

  Next unique index for creating ENodes

• newRawFacts : Std.Queue NewRawFact

  new facts to be preprocessed and then asserted.

• facts : PArray Expr

  Asserted facts

• extThms : PHashMap ExprPtr (Array Ext.ExtTheorem)

  Cached extensionality theorems for types.

• ematch : EMatch.State

  State of the E-matching module.

• inj : Injective.State

  State of the injective function procedure.

• split : Split.State

  State of the case-splitting module.

• clean : Clean.State

  State of the clean name generator.

• sstates : Array SolverExtensionState

  Solver states.

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedGoalState : Inhabited GoalState

def Lean.Meta.Grind.instInhabitedGoalState.default : GoalState

structure Lean.Meta.Grind.Goalextends Lean.Meta.Grind.GoalState : Type

A grind goal, combining shared state with a specific metavariable.

See GoalState for details on why the state is factored out. Note: The Goal internal representation is just a pair GoalState and MVarId.

• nextDeclIdx : Nat
• canon : Canon.State
• enodeMap : ENodeMap
• exprs : PArray Expr
• parents : ParentMap
• congrTable : CongrTable self.enodeMap
• appMap : PHashMap HeadIndex (List Expr)
• indicesFound : PHashSet HeadIndex
• newFacts : Array NewFact
• inconsistent : Bool
• nextIdx : Nat
• newRawFacts : Std.Queue NewRawFact
• facts : PArray Expr
• extThms : PHashMap ExprPtr (Array Ext.ExtTheorem)
• ematch : EMatch.State
• inj : Injective.State
• split : Split.State
• clean : Clean.State
• sstates : Array SolverExtensionState
• mvarId : MVarId

def Lean.Meta.Grind.instInhabitedGoal.default : Goal

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedGoal : Inhabited Goal

def Lean.Meta.Grind.Goal.hasSameRoot (g : Goal) (a b : Expr) : Bool

def Lean.Meta.Grind.Goal.isCongruent (g : Goal) (a b : Expr) : Bool

def Lean.Meta.Grind.Goal.admit (goal : Goal) : MetaM Unit

@[reducible, inline]

abbrev Lean.Meta.Grind.GoalM (α : Type) : Type

@[inline]

def Lean.Meta.Grind.GoalM.runCore {α : Type} (goal : Goal) (x : GoalM α) : GrindM (α × Goal)

@[inline]

def Lean.Meta.Grind.GoalM.run {α : Type} (goal : Goal) (x : GoalM α) : GrindM (α × Goal)

@[inline]

def Lean.Meta.Grind.GoalM.run' (goal : Goal) (x : GoalM Unit) : GrindM Goal

def Lean.Meta.Grind.Goal.setNextDeclToEnd (g : Goal) : MetaM Goal

Sets nextDeclIdx to point past the last local declaration in the local context.

This marks all existing local declarations as already processed by grind. Use this when initializing a goal whose hypotheses should not be processed or after internalizing all of them.

def Lean.Meta.Grind.setNextDeclToEnd : GoalM Unit

def Lean.Meta.Grind.Goal.hasPendingLocalDecls (g : Goal) : MetaM Bool

Returns true if the goal has local declarations that have not yet been processed by grind.

A local declaration is "pending" if its index is greater than or equal to nextDeclIdx. This is used to determine whether grind needs to internalize new hypotheses.

def Lean.Meta.Grind.updateLastTag : GoalM Unit

def Lean.Meta.Grind.«doElemTrace_goal[_]__» : ParserDescr

Macro similar to trace[...], but it includes the trace message trace[grind] "working on <current goal>" if the tag has changed since the last trace message.

def Lean.Meta.Grind.markTheoremInstance (proof : Expr) (assignment : Array Expr) : GoalM Bool

A helper function used to mark a theorem instance found by the E-matching module. It returns true if it is a new instance and false otherwise.

def Lean.Meta.Grind.addNewRawFact (proof prop : Expr) (generation : Nat) (splitSource : SplitSource) : GoalM Unit

Adds a new fact prop with proof proof to the queue for preprocessing and the assertion.

def Lean.Meta.Grind.getNumTheoremInstances : GoalM Nat

Returns the number of theorem instances generated so far.

def Lean.Meta.Grind.checkMaxInstancesExceeded : GoalM Bool

Returns true if the maximum number of instances has been reached.

def Lean.Meta.Grind.checkMaxCaseSplit : GoalM Bool

Returns true if the maximum number of case-splits has been reached.

def Lean.Meta.Grind.checkMaxEmatchExceeded : GoalM Bool

Returns true if the maximum number of E-matching rounds has been reached.

def Lean.Meta.Grind.Goal.getENode? (goal : Goal) (e : Expr) : Option ENode

Returns some n if e has already been "internalized" into the Otherwise, returns nones.

@[inline]

def Lean.Meta.Grind.getENode? (e : Expr) : GoalM (Option ENode)

Returns some n if e has already been "internalized" into the Otherwise, returns nones.

def Lean.Meta.Grind.throwNonInternalizedExpr {α : Type} (e : Expr) : MetaM α

def Lean.Meta.Grind.Goal.getENode (goal : Goal) (e : Expr) : MetaM ENode

Returns node associated with e. It assumes e has already been internalized.

@[inline]

def Lean.Meta.Grind.getENode (e : Expr) : GoalM ENode

Returns node associated with e. It assumes e has already been internalized.

def Lean.Meta.Grind.Goal.getGeneration (goal : Goal) (e : Expr) : Nat

def Lean.Meta.Grind.SplitInfo.getGenerationCore (goal : Goal) : SplitInfo → Nat

def Lean.Meta.Grind.SplitInfo.getGeneration (s : SplitInfo) : GoalM Nat

def Lean.Meta.Grind.getGeneration (e : Expr) : GoalM Nat

Returns the generation of the given term. Is assumes it has been internalized

def Lean.Meta.Grind.isEqTrue (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of True.

def Lean.Meta.Grind.isEqFalse (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of False.

def Lean.Meta.Grind.isEqBoolTrue (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of Bool.true.

def Lean.Meta.Grind.isEqBoolFalse (e : Expr) : GoalM Bool

Returns true if e is in the equivalence class of Bool.false.

def Lean.Meta.Grind.isEqv (a b : Expr) : GoalM Bool

Returns true if a and b are in the same equivalence class.

def Lean.Meta.Grind.isRoot (e : Expr) : GoalM Bool

Returns true if the root of its equivalence class.

def Lean.Meta.Grind.Goal.getRoot? (goal : Goal) (e : Expr) : Option Expr

Returns the root element in the equivalence class of e IF e has been internalized.

@[inline]

def Lean.Meta.Grind.getRoot? (e : Expr) : GoalM (Option Expr)

Returns the root element in the equivalence class of e IF e has been internalized.

def Lean.Meta.Grind.Goal.getRoot (goal : Goal) (e : Expr) : MetaM Expr

Returns the root element in the equivalence class of e.

@[inline]

def Lean.Meta.Grind.getRoot (e : Expr) : GoalM Expr

Returns the root element in the equivalence class of e.

def Lean.Meta.Grind.getRootENode (e : Expr) : GoalM ENode

Returns the root enode in the equivalence class of e.

def Lean.Meta.Grind.getRootENode? (e : Expr) : GoalM (Option ENode)

Returns the root enode in the equivalence class of e if it is in an equivalence class.

def Lean.Meta.Grind.useFunCC (e : Expr) : GoalM Bool

Returns true if the ENode associate with e has support for function equality congruence closure. See Grind.Config.funCC for additional details.

def Lean.Meta.Grind.Goal.getNext? (goal : Goal) (e : Expr) : Option Expr

Returns the next element in the equivalence class of e if e has been internalized in the given goal.

def Lean.Meta.Grind.Goal.getNext (goal : Goal) (e : Expr) : MetaM Expr

Returns the next element in the equivalence class of e.

@[inline]

def Lean.Meta.Grind.getNext (e : Expr) : GoalM Expr

Returns the root element in the equivalence class of e.

def Lean.Meta.Grind.alreadyInternalized (e : Expr) : GoalM Bool

Returns true if e has already been internalized.

def Lean.Meta.Grind.Goal.getTarget? (goal : Goal) (e : Expr) : Option Expr

@[inline]

def Lean.Meta.Grind.getTarget? (e : Expr) : GoalM (Option Expr)

def Lean.Meta.Grind.pushEqCore (lhs rhs proof : Expr) (isHEq : Bool) : GoalM Unit

If isHEq is false, it pushes lhs = rhs with proof to newEqs. Otherwise, it pushes lhs ≍ rhs.

def Lean.Meta.Grind.hasSameType (a b : Expr) : MetaM Bool

Return true if a and b have the same type.

@[inline]

def Lean.Meta.Grind.pushEqHEq (lhs rhs proof : Expr) : GoalM Unit

@[inline]

def Lean.Meta.Grind.pushEq (lhs rhs proof : Expr) : GoalM Unit

Pushes lhs = rhs with proof to newEqs.

@[inline]

def Lean.Meta.Grind.pushHEq (lhs rhs proof : Expr) : GoalM Unit

Pushes lhs ≍ rhs with proof to newEqs.

def Lean.Meta.Grind.pushEqTrue (a proof : Expr) : GoalM Unit

Pushes a = True with proof to newEqs.

def Lean.Meta.Grind.pushEqFalse (a proof : Expr) : GoalM Unit

Pushes a = False with proof to newEqs.

def Lean.Meta.Grind.pushEqBoolTrue (a proof : Expr) : GoalM Unit

Pushes a = Bool.true with proof to newEqs.

def Lean.Meta.Grind.pushEqBoolFalse (a proof : Expr) : GoalM Unit

Pushes a = Bool.false with proof to newEqs.

def Lean.Meta.Grind.registerParent (parent child : Expr) : GoalM Unit

Records that parent is a parent of child. This function actually stores the information in the root (aka canonical representative) of child.

def Lean.Meta.Grind.getParents (e : Expr) : GoalM ParentSet

Returns the set of expressions e is a child of, or an expression in es equivalence class is a child of. The information is only up to date if e is the root (aka canonical representative) of the equivalence class.

def Lean.Meta.Grind.resetParentsOf (e : Expr) : GoalM Unit

Removes the entry e ↦ parents from the parent map.

def Lean.Meta.Grind.copyParentsTo (parents : ParentSet) (root : Expr) : GoalM Unit

Copy parents to the parents of root. root must be the root of its equivalence class.

def Lean.Meta.Grind.mkENodeCore (e : Expr) (interpreted ctor : Bool) (generation : Nat) (funCC : Bool) : GoalM Unit

def Lean.Meta.Grind.mkENode (e : Expr) (generation : Nat) (funCC : Bool := false) : GoalM Unit

Creates an ENode for e if one does not already exist. This method assumes e has been hash-consed.

def Lean.Meta.Grind.setENode (e : Expr) (n : ENode) : GoalM Unit

def Lean.Meta.Grind.hasType (t α : Expr) : MetaM Bool

Returns true if type of t is definitionally equal to α

@[inline]

def Lean.Meta.Grind.forEachDiseq (parents : ParentSet) (k : Expr → Expr → GoalM Unit) : GoalM Unit

For each equality b = c in parents, executes k b c IF

• b = c is equal to False, and

def Lean.Meta.Grind.isCongrRoot (e : Expr) : GoalM Bool

Returns true is e is the root of its congruence class.

partial def Lean.Meta.Grind.getCongrRoot (e : Expr) : GoalM Expr

Returns the root of the congruence class containing e.

def Lean.Meta.Grind.isInconsistent : GoalM Bool

Return true if the goal is inconsistent.

@[extern lean_grind_mk_eq_proof]

opaque Lean.Meta.Grind.mkEqProof (a b : Expr) : GoalM Expr

Returns a proof that a = b. It assumes a and b are in the same equivalence class, and have the same type.

@[extern lean_grind_mk_heq_proof]

opaque Lean.Meta.Grind.mkHEqProof (a b : Expr) : GoalM Expr

Returns a proof that a ≍ b. It assumes a and b are in the same equivalence class.

@[extern lean_grind_process_new_facts]

opaque Lean.Meta.Grind.processNewFacts : GoalM Unit

@[extern lean_grind_internalize]

opaque Lean.Meta.Grind.internalize (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit

@[extern lean_grind_preprocess]

opaque Lean.Meta.Grind.preprocess : Expr → GoalM Simp.Result

def Lean.Meta.Grind.internalizeLocalDecl (localDecl : LocalDecl) : GoalM Unit

Internalizes a local declaration which is not a proposition. Note: We must internalize local variables because their types may be empty, and may not be referenced anywhere else. Example:

example (a : { x : Int // x < 0 ∧ x > 0 }) : False := by grind

etaStruct may also be applicable.

def Lean.Meta.Grind.mkEqHEqProof (a b : Expr) : GoalM Expr

Returns a proof that a = b if they have the same type. Otherwise, returns a proof of a ≍ b. It assumes a and b are in the same equivalence class.

def Lean.Meta.Grind.mkEqTrueProof (a : Expr) : GoalM Expr

Returns a proof that a = True. It assumes a and True are in the same equivalence class.

def Lean.Meta.Grind.mkEqFalseProof (a : Expr) : GoalM Expr

Returns a proof that a = False. It assumes a and False are in the same equivalence class.

def Lean.Meta.Grind.mkEqBoolTrueProof (a : Expr) : GoalM Expr

Returns a proof that a = Bool.true. It assumes a and Bool.true are in the same equivalence class.

def Lean.Meta.Grind.mkEqBoolFalseProof (a : Expr) : GoalM Expr

Returns a proof that a = Bool.false. It assumes a and Bool.false are in the same equivalence class.

def Lean.Meta.Grind.markAsInconsistent : GoalM Unit

Marks current goal as inconsistent without assigning mvarId.

def Lean.MVarId.assignFalseProof (mvarId : MVarId) (falseProof : Expr) : MetaM Unit

Assign the mvarId using the given proof of False. If type of mvarId is not False, then use False.elim.

@[inline]

def Lean.Meta.Grind.Goal.withContext {m : Type → Type u_1} {α : Type} [MonadControlT MetaM m] [Monad m] (goal : Goal) : m α → m α

goal.withContext x executes x using the given metavariable LocalContext and LocalInstances. The type class resolution cache is flushed when executing x if its LocalInstances are different from the current ones.

def Lean.Meta.Grind.Goal.mkAuxMVar (goal : Goal) : MetaM MVarId

Creates an auxiliary metavariable with the same type and context of goal.mvarId. We use this function to perform cases on the current goal without eagerly assigning it.

def Lean.Meta.Grind.closeGoal (falseProof : Expr) : GoalM Unit

Closes the current goal using the given proof of False and marks it as inconsistent if it is not already marked so.

def Lean.Meta.Grind.getExprs : GoalM (PArray Expr)

Returns all enodes in the goal

@[inline]

def Lean.Meta.Grind.traverseEqc (e : Expr) (f : ENode → GoalM Unit) : GoalM Unit

Executes f to each term in the equivalence class containing e

@[inline]

def Lean.Meta.Grind.findEqc (e : Expr) (f : ENode → GoalM Bool) : GoalM Bool

Executes f to each term in the equivalence class containing e, and stops as soon as f returns true.

@[inline]

def Lean.Meta.Grind.foldEqc {α : Type} (e : Expr) (init : α) (f : ENode → α → GoalM α) : GoalM α

Folds using f and init over the equivalence class containing e

def Lean.Meta.Grind.forEachENode (f : ENode → GoalM Unit) : GoalM Unit

def Lean.Meta.Grind.filterENodes (p : ENode → GoalM Bool) : GoalM (Array ENode)

def Lean.Meta.Grind.forEachEqcRoot (f : ENode → GoalM Unit) : GoalM Unit

@[reducible, inline]

abbrev Lean.Meta.Grind.Propagator : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.EvalTactic : Type

def Lean.Meta.Grind.EvalTactic.skip : EvalTactic

structure Lean.Meta.Grind.Methods : Type

• propagateUp : Propagator
• propagateDown : Propagator
• evalTactic : EvalTactic

def Lean.Meta.Grind.instInhabitedMethods.default : Methods

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedMethods : Inhabited Methods

def Lean.Meta.Grind.Methods.toMethodsRef (m : Methods) : MethodsRef

@[inline]

def Lean.Meta.Grind.getMethods : GrindM Methods

def Lean.Meta.Grind.propagateUp (e : Expr) : GoalM Unit

def Lean.Meta.Grind.propagateDown (e : Expr) : GoalM Unit

def Lean.Meta.Grind.evalTactic (goal : Goal) (stx : TSyntax `grind) : GrindM (List Goal)

def Lean.Meta.Grind.Goal.getEqc (goal : Goal) (e : Expr) (sort : Bool := false) : List Expr

Returns expressions in the given expression equivalence class.

@[inline]

def Lean.Meta.Grind.getEqc (e : Expr) (sort : Bool := false) : GoalM (List Expr)

Returns expressions in the given expression equivalence class.

def Lean.Meta.Grind.Goal.getEqcs (goal : Goal) (sort : Bool := false) : List (List Expr)

Returns all equivalence classes in the current goal.

@[inline]

def Lean.Meta.Grind.getEqcs : GoalM (List (List Expr))

Returns all equivalence classes in the current goal.

def Lean.Meta.Grind.isKnownCaseSplit (s : SplitInfo) : GoalM Bool

Returns true if s has been already added to the case-split list at one point. Remark: this function returns true even if the split has already been resolved and is not in the list anymore.

def Lean.Meta.Grind.isResolvedCaseSplit (e : Expr) : GoalM Bool

Returns true if e is a case-split that does not need to be performed anymore.

def Lean.Meta.Grind.markCaseSplitAsResolved (e : Expr) : GoalM Unit

Marks e as a case-split that does not need to be performed anymore. Remark: we currently use this feature to disable match-case-splits. Remark: we also use this feature to record the case-splits that have already been performed.

def Lean.Meta.Grind.addSplitCandidate (sinfo : SplitInfo) : GoalM Unit

Inserts e into the list of case-split candidates if it was not inserted before.

inductive Lean.Meta.Grind.ActivateNextGuardResult : Type

• ready : ActivateNextGuardResult
• next (guard : Expr) (pending : List TheoremGuard) : ActivateNextGuardResult

def Lean.Meta.Grind.activateNextGuard (thm : EMatchTheorem) (guards : List TheoremGuard) (generation : Nat) : GoalM ActivateNextGuardResult

def Lean.Meta.Grind.addTheoremInstance (thm : EMatchTheorem) (proof prop : Expr) (generation : Nat) (guards : List TheoremGuard) : GoalM Unit

Adds a new theorem instance produced using E-matching.

def Lean.Meta.Grind.DelayedTheoremInstance.check (delayed : DelayedTheoremInstance) : GoalM Unit

def Lean.Meta.Grind.getExtTheorems (type : Expr) : GoalM (Array Ext.ExtTheorem)

Returns extensionality theorems for the given type if available. If Config.ext is false, the result is #[].

def Lean.Meta.Grind.addLookaheadCandidate (sinfo : SplitInfo) : GoalM Unit

Add a new lookahead candidate.

def Lean.Meta.Grind.withoutModifyingState {α : Type} (x : GoalM α) : GoalM α

Helper function for executing x with a fresh newFacts and without modifying the goal state.

@[extern lean_grind_canon]

opaque Lean.Meta.Grind.canon (e : Expr) : GoalM Expr

Canonicalizes nested types, type formers, and instances in e.

Action is the control interface for grind’s search steps. It is defined in Continuation-Passing Style (CPS). See Grind/Action.lean for additional details.

@[reducible, inline]

abbrev Lean.Meta.Grind.TGrind : Type

inductive Lean.Meta.Grind.ActionResult : Type

Result type for a grind Action

• closed (seq : List TGrind) : ActionResult

  The goal has been closed, and you can use seq to close the goal efficiently.

• stuck (gs : List Goal) : ActionResult

  The action could not make further progress. gs are subgoals that could not be closed. They are used for producing error messages.

def Lean.Meta.Grind.instInhabitedActionResult.default : ActionResult

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedActionResult : Inhabited ActionResult

@[reducible, inline]

abbrev Lean.Meta.Grind.ActionCont : Type

@[reducible, inline]

abbrev Lean.Meta.Grind.Action : Type

def Lean.Meta.Grind.Action.notApplicable : Action

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedAction : Inhabited Action

Solver Extensions

structure Lean.Meta.Grind.SolverExtension (σ : Type) : Type

Solver extension, can only be generated by registerSolverExtension that allocates a unique index for this extension into each goal's extension state's array.

• id : Nat
• mkInitial : IO σ
• internalize : Expr → (parent? : Option Expr) → GoalM Unit
• newEq : Expr → Expr → GoalM Unit
• newDiseq : Expr → Expr → GoalM Unit
• mbtc : GoalM Bool
• action : Action
• check : GoalM Bool
• checkInv : GoalM Unit

def Lean.Meta.Grind.instInhabitedSolverExtension.default {a✝ : Type} : SolverExtension a✝

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedSolverExtension {a✝ : Type} : Inhabited (SolverExtension a✝)

def Lean.Meta.Grind.registerSolverExtension {σ : Type} (mkInitial : IO σ) : IO (SolverExtension σ)

Registers a new solver extension for grind. Solver extensions can only be registered during initialization. Reason: We do not use any synchronization primitive to access solverExtensionsRef.

def Lean.Meta.Grind.SolverExtension.setMethods {σ : Type} (ext : SolverExtension σ) (internalize : Expr → Option Expr → GoalM Unit := fun (x : Expr) (x_1 : Option Expr) => pure ()) (newEq newDiseq : Expr → Expr → GoalM Unit := fun (x x_1 : Expr) => pure ()) (mbtc : GoalM Bool := pure false) (action : Action := Action.notApplicable) (check : GoalM Bool := pure false) (checkInv : GoalM Unit := pure ()) : IO Unit

Sets methods/handlers for solver extension ext. Solver extension methods can only be registered during initialization. Reason: We do not use any synchronization primitive to access solverExtensionsRef.

def Lean.Meta.Grind.Solvers.mkInitialStates : IO (Array SolverExtensionState)

Returns initial state for registered solvers.

@[implicit_reducible]

instance Lean.Meta.Grind.instInhabitedGoalM {σ : Type} : Inhabited (GoalM σ)

@[implemented_by _private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.modifyStateImpl]

opaque Lean.Meta.Grind.SolverExtension.modifyState {σ : Type} (ext : SolverExtension σ) (f : σ → σ) : GoalM Unit

@[implemented_by _private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.SolverExtension.getStateCoreImpl]

opaque Lean.Meta.Grind.SolverExtension.getStateCore {σ : Type} (ext : SolverExtension σ) (goal : Goal) : IO σ

def Lean.Meta.Grind.SolverExtension.getState {σ : Type} (ext : SolverExtension σ) : GoalM σ

def Lean.Meta.Grind.Solvers.internalize (e : Expr) (parent? : Option Expr) : GoalM Unit

Internalizes given expression in all registered solvers.

def Lean.Meta.Grind.Solvers.checkInvariants : GoalM Unit

Checks invariants of all registered solvers.

def Lean.Meta.Grind.Solvers.check? : GoalM (Option (Array Nat))

Performs (expensive) satisfiability checks in all registered solvers, and returns the solver ids that made progress.

def Lean.Meta.Grind.Solvers.check : GoalM Bool

def Lean.Meta.Grind.Solvers.mbtc : GoalM Bool

Invokes model-based theory combination extensions in all registered solvers.

def Lean.Meta.Grind.Action.andAlso (x y : Action) : Action

Sequential conjunction: executes both x and y.

• Runs x and always runs y afterward, regardless of whether x made progress.
• It is not applicable only if both x and y are not applicable.

def Lean.Meta.Grind.Solvers.mkAction : IO Action

def Lean.Meta.Grind.Solvers.propagateDiseqs (lhs rhs : Expr) : GoalM Unit

Given a new disequality lhs ≠ rhs, propagates it to relevant theories.

def Lean.Meta.Grind.isSameSolverTerms (a b : SolverTerms) : Bool

def Lean.Meta.Grind.SolverExtension.markTerm {σ : Type} (ext : SolverExtension σ) (e : Expr) : GoalM Unit

def Lean.Meta.Grind.SolverExtension.getTerm {σ : Type} (ext : SolverExtension σ) (e : ENode) : Option Expr

Returns some t if t is the solver term for ext associated with e.

def Lean.Meta.Grind.SolverExtension.hasTermAtRoot {σ : Type} (ext : SolverExtension σ) (e : Expr) : GoalM Bool

Returns true if the root of es equivalence class is already attached to a term of the given solver.

structure Lean.Meta.Grind.PendingSolverPropagations : Type

• data : Lean.Meta.Grind.PendingSolverPropagationsData✝

def Lean.Meta.Grind.Solvers.mergeTerms (rhsRoot lhsRoot : ENode) : GoalM PendingSolverPropagations

def Lean.Meta.Grind.PendingSolverPropagations.propagate (p : PendingSolverPropagations) : GoalM Unit

def Lean.Meta.Grind.anchorPrefixToString (numDigits : Nat) (anchorPrefix : UInt64) : String

def Lean.Meta.Grind.anchorToString (numDigits : Nat) (anchor : UInt64) : String

def Lean.Meta.Grind.AnchorRef.toString (anchorRef : AnchorRef) : String

@[implicit_reducible]

instance Lean.Meta.Grind.instToStringAnchorRef : ToString AnchorRef

def Lean.Meta.Grind.Goal.getActiveMatchEqTheorems (goal : Goal) : CoreM (Array EMatchTheorem)

Returns activated match-declaration equations. Recall that in tactics such as instantiate only [...], match-declarations are always instantiated.