structure Lean.Meta.Grind.CasesTypes : Type

Types that grind will case-split on.

• casesMap : PHashMap Name Bool

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedCasesTypes : Inhabited CasesTypes

def Lean.Meta.Grind.CasesTypes.insert (s : CasesTypes) (declName : Name) (eager : Bool) : CasesTypes

@[reducible, inline]

abbrev Lean.Meta.Grind.ExtTheorems : Type

structure Lean.Meta.Grind.SymbolPriorities : Type

• map : PHashMap Name Nat

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedSymbolPriorities : Inhabited SymbolPriorities

def Lean.Meta.Grind.SymbolPriorities.insert (s : SymbolPriorities) (declName : Name) (prio : Nat) : SymbolPriorities

Inserts declName ↦ prio into s.

inductive Lean.Meta.Grind.EMatchTheoremKind : Type

• eqLhs (gen : Bool) : EMatchTheoremKind
• eqRhs (gen : Bool) : EMatchTheoremKind
• eqBoth (gen : Bool) : EMatchTheoremKind
• eqBwd : EMatchTheoremKind
• fwd : EMatchTheoremKind
• bwd (gen : Bool) : EMatchTheoremKind
• leftRight : EMatchTheoremKind
• rightLeft : EMatchTheoremKind
• default (gen : Bool) : EMatchTheoremKind
• user : EMatchTheoremKind

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind : Inhabited EMatchTheoremKind

@[instance_reducible]

instance Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq EMatchTheoremKind

def Lean.Meta.Grind.instBEqEMatchTheoremKind.beq : EMatchTheoremKind → EMatchTheoremKind → Bool

@[instance_reducible]

instance Lean.Meta.Grind.instReprEMatchTheoremKind : Repr EMatchTheoremKind

def Lean.Meta.Grind.instReprEMatchTheoremKind.repr : EMatchTheoremKind → Nat → Format

@[instance_reducible]

instance Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable EMatchTheoremKind

def Lean.Meta.Grind.instHashableEMatchTheoremKind.hash : EMatchTheoremKind → UInt64

structure Lean.Meta.Grind.CnstrRHS : Type

• levelNames : Array Name

  Abstracted universe level param names in the rhs

• numMVars : Nat

  Number of abstracted metavariable in the rhs

• expr : Expr

  The actual rhs.

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedCnstrRHS : Inhabited CnstrRHS

def Lean.Meta.Grind.instBEqCnstrRHS.beq : CnstrRHS → CnstrRHS → Bool

@[instance_reducible]

instance Lean.Meta.Grind.instBEqCnstrRHS : BEq CnstrRHS

def Lean.Meta.Grind.instReprCnstrRHS.repr : CnstrRHS → Nat → Format

@[instance_reducible]

instance Lean.Meta.Grind.instReprCnstrRHS : Repr CnstrRHS

inductive Lean.Meta.Grind.EMatchTheoremConstraint : Type

Grind patterns may have constraints associated with them.

• notDefEq (lhs : Nat) (rhs : CnstrRHS) : EMatchTheoremConstraint

  A constraint of the form lhs =/= rhs. The lhs is one of the bound variables, and the rhs an abstract term that must not be definitionally equal to a term t assigned to lhs.

• defEq (lhs : Nat) (rhs : CnstrRHS) : EMatchTheoremConstraint

  A constraint of the form lhs =?= rhs. The lhs is one of the bound variables, and the rhs an abstract term that must be definitionally equal to a term t assigned to lhs.

• sizeLt (lhs n : Nat) : EMatchTheoremConstraint

  A constraint of the form size lhs < n. The lhs is one of the bound variables. The size is computed ignoring implicit terms, but sharing is not taken into account.

• depthLt (lhs n : Nat) : EMatchTheoremConstraint

  A constraint of the form depth lhs < n. The lhs is one of the bound variables. The depth is computed in constant time using the approxDepth field attached to expressions.

• genLt (n : Nat) : EMatchTheoremConstraint

  Instantiates the theorem only if its generation is less than n

• isGround (bvarIdx : Nat) : EMatchTheoremConstraint

  Constraints of the form is_ground x. Instantiates the theorem only if x is ground term.

• isValue (bvarIdx : Nat) (strict : Bool) : EMatchTheoremConstraint

  Constraints of the form is_value x and is_strict_value x. A value is defined as

  • A constructor fully applied to value arguments.
  • A literal: numerals, strings, etc.
  • A lambda. In the strict case, lambdas are not considered.
• maxInsts (n : Nat) : EMatchTheoremConstraint

  Instantiates the theorem only if less than n instances have been generated for this theorem.

• guard (e : Expr) : EMatchTheoremConstraint

  It instructs grind to postpone the instantiation of the theorem until e is known to be true.

• check (e : Expr) : EMatchTheoremConstraint

  Similar to guard, but checks whether e is implied by asserting ¬e.

• notValue (bvarIdx : Nat) (strict : Bool) : EMatchTheoremConstraint

  Constraints of the form not_value x and not_strict_value x. They are the negations of is_value x and is_strict_value x.

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint : Inhabited EMatchTheoremConstraint

@[instance_reducible]

instance Lean.Meta.Grind.instReprEMatchTheoremConstraint : Repr EMatchTheoremConstraint

def Lean.Meta.Grind.instReprEMatchTheoremConstraint.repr : EMatchTheoremConstraint → Nat → Format

def Lean.Meta.Grind.instBEqEMatchTheoremConstraint.beq : EMatchTheoremConstraint → EMatchTheoremConstraint → Bool

@[instance_reducible]

instance Lean.Meta.Grind.instBEqEMatchTheoremConstraint : BEq EMatchTheoremConstraint

structure Lean.Meta.Grind.EMatchTheorem : Type

A theorem for heuristic instantiation based on E-matching.

• levelParams : Array Name

  It stores universe parameter names for universe polymorphic proofs. Recall that it is non-empty only when we elaborate an expression provided by the user. When proof is just a constant, we can use the universe parameter names stored in the declaration.

• proof : Expr
• numParams : Nat
• patterns : List Expr
• symbols : List HeadIndex

  Contains all symbols used in patterns.

• origin : Origin
• kind : EMatchTheoremKind

  The kind is used for generating the patterns. We save it here to implement grind?.

• minIndexable : Bool

  Stores whether patterns were inferred using the minimal indexable subexpression condition.

• cnstrs : List EMatchTheoremConstraint

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited EMatchTheorem

@[instance_reducible]

instance Lean.Meta.Grind.instTheoremLikeEMatchTheorem : TheoremLike EMatchTheorem

structure Lean.Meta.Grind.InjectiveTheorem : Type

A theorem marked with @[grind inj]

• levelParams : Array Name
• proof : Expr
• symbols : List HeadIndex

  Contains all symbols used in the term f at the theorem's conclusion: Function.Injective f.

• origin : Origin

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedInjectiveTheorem : Inhabited InjectiveTheorem

@[instance_reducible]

instance Lean.Meta.Grind.instTheoremLikeInjectiveTheorem : TheoremLike InjectiveTheorem

inductive Lean.Meta.Grind.Entry : Type

• ext (declName : Name) : Entry
• funCC (declName : Name) : Entry
• cases (declName : Name) (eager : Bool) : Entry
• ematch (thm : EMatchTheorem) : Entry
• inj (thm : InjectiveTheorem) : Entry

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedEntry : Inhabited Entry

structure Lean.Meta.Grind.ExtensionState : Type

• casesTypes : CasesTypes
• extThms : ExtTheorems
• funCC : NameSet
• ematch : Theorems EMatchTheorem
• inj : Theorems InjectiveTheorem

@[instance_reducible]

instance Lean.Meta.Grind.instInhabitedExtensionState : Inhabited ExtensionState

@[reducible, inline]

abbrev Lean.Meta.Grind.Extension : Type

def Lean.Meta.Grind.ExtensionState.addEntry (s : ExtensionState) (e : Entry) : ExtensionState

def Lean.Meta.Grind.mkExtension (name : Name := by exact decl_name%) : IO Extension

@[reducible, inline]

abbrev Lean.Meta.Grind.ExtensionStateArray : Type

grind is parametrized by a collection of ExtensionState. The motivation is to allow users to use multiple extensions simultaneously without merging them into a single structure. The collection is scanned linearly. In practice, we expect the array to be very small.

def Lean.Meta.Grind.throwNotMarkedWithGrindAttribute {α : Type} (declName : Name) : CoreM α