structure Lean.Meta.Grind.CasesTypes : Type

Types that grind will case-split on.

• casesMap : PHashMap Name Bool

instance Lean.Meta.Grind.instInhabitedCasesTypes : Inhabited CasesTypes

Equations

• Lean.Meta.Grind.instInhabitedCasesTypes = { default := Lean.Meta.Grind.instInhabitedCasesTypes.default }

def Lean.Meta.Grind.instInhabitedCasesTypes.default : CasesTypes

Equations

• Lean.Meta.Grind.instInhabitedCasesTypes.default = { casesMap := default }

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

Equations

• s.insert declName eager = { casesMap := Lean.PersistentHashMap.insert s.casesMap declName eager }

@[reducible, inline]

abbrev Lean.Meta.Grind.ExtTheorems : Type

Equations

• Lean.Meta.Grind.ExtTheorems = Lean.PHashSet Lean.Name

structure Lean.Meta.Grind.SymbolPriorities : Type

• map : PHashMap Name Nat

def Lean.Meta.Grind.instInhabitedSymbolPriorities.default : SymbolPriorities

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorities.default = { map := default }

instance Lean.Meta.Grind.instInhabitedSymbolPriorities : Inhabited SymbolPriorities

Equations

• Lean.Meta.Grind.instInhabitedSymbolPriorities = { default := Lean.Meta.Grind.instInhabitedSymbolPriorities.default }

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

Inserts declName ↦ prio into s.

Equations

• s.insert declName prio = { map := Lean.PersistentHashMap.insert s.map declName prio }

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

def Lean.Meta.Grind.instInhabitedEMatchTheoremKind.default : EMatchTheoremKind

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremKind.default = Lean.Meta.Grind.EMatchTheoremKind.eqLhs default

instance Lean.Meta.Grind.instInhabitedEMatchTheoremKind : Inhabited EMatchTheoremKind

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremKind = { default := Lean.Meta.Grind.instInhabitedEMatchTheoremKind.default }

instance Lean.Meta.Grind.instBEqEMatchTheoremKind : BEq EMatchTheoremKind

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremKind = { beq := Lean.Meta.Grind.instBEqEMatchTheoremKind.beq }

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

Equations

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

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

Equations

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

instance Lean.Meta.Grind.instReprEMatchTheoremKind : Repr EMatchTheoremKind

Equations

• Lean.Meta.Grind.instReprEMatchTheoremKind = { reprPrec := Lean.Meta.Grind.instReprEMatchTheoremKind.repr }

instance Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable EMatchTheoremKind

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremKind = { hash := Lean.Meta.Grind.instHashableEMatchTheoremKind.hash }

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

Equations

• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.eqLhs a) = mixHash 0 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.eqRhs a) = mixHash 1 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.eqBoth a) = mixHash 2 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.eqBwd = 3
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.fwd = 4
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.bwd a) = mixHash 5 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.leftRight = 6
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.rightLeft = 7
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash (Lean.Meta.Grind.EMatchTheoremKind.default a) = mixHash 8 (hash a)
• Lean.Meta.Grind.instHashableEMatchTheoremKind.hash Lean.Meta.Grind.EMatchTheoremKind.user = 9

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 Lean.Meta.Grind.instInhabitedCnstrRHS : Inhabited CnstrRHS

Equations

• Lean.Meta.Grind.instInhabitedCnstrRHS = { default := Lean.Meta.Grind.instInhabitedCnstrRHS.default }

def Lean.Meta.Grind.instInhabitedCnstrRHS.default : CnstrRHS

Equations

• Lean.Meta.Grind.instInhabitedCnstrRHS.default = { levelNames := default, numMVars := default, expr := default }

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

Equations

• Lean.Meta.Grind.instBEqCnstrRHS.beq { levelNames := a, numMVars := a_1, expr := a_2 } { levelNames := b, numMVars := b_1, expr := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.Grind.instBEqCnstrRHS.beq x✝¹ x✝ = false

instance Lean.Meta.Grind.instBEqCnstrRHS : BEq CnstrRHS

Equations

• Lean.Meta.Grind.instBEqCnstrRHS = { beq := Lean.Meta.Grind.instBEqCnstrRHS.beq }

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

Equations

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

instance Lean.Meta.Grind.instReprCnstrRHS : Repr CnstrRHS

Equations

• Lean.Meta.Grind.instReprCnstrRHS = { reprPrec := Lean.Meta.Grind.instReprCnstrRHS.repr }

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.

def Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint.default : EMatchTheoremConstraint

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint.default = Lean.Meta.Grind.EMatchTheoremConstraint.notDefEq default default

instance Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint : Inhabited EMatchTheoremConstraint

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint = { default := Lean.Meta.Grind.instInhabitedEMatchTheoremConstraint.default }

instance Lean.Meta.Grind.instReprEMatchTheoremConstraint : Repr EMatchTheoremConstraint

Equations

• Lean.Meta.Grind.instReprEMatchTheoremConstraint = { reprPrec := Lean.Meta.Grind.instReprEMatchTheoremConstraint.repr }

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

Equations

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

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

Equations

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

instance Lean.Meta.Grind.instBEqEMatchTheoremConstraint : BEq EMatchTheoremConstraint

Equations

• Lean.Meta.Grind.instBEqEMatchTheoremConstraint = { beq := Lean.Meta.Grind.instBEqEMatchTheoremConstraint.beq }

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

def Lean.Meta.Grind.instInhabitedEMatchTheorem.default : EMatchTheorem

Equations

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

instance Lean.Meta.Grind.instInhabitedEMatchTheorem : Inhabited EMatchTheorem

Equations

• Lean.Meta.Grind.instInhabitedEMatchTheorem = { default := Lean.Meta.Grind.instInhabitedEMatchTheorem.default }

instance Lean.Meta.Grind.instTheoremLikeEMatchTheorem : TheoremLike EMatchTheorem

Equations

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

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 Lean.Meta.Grind.instInhabitedInjectiveTheorem : Inhabited InjectiveTheorem

Equations

• Lean.Meta.Grind.instInhabitedInjectiveTheorem = { default := Lean.Meta.Grind.instInhabitedInjectiveTheorem.default }

def Lean.Meta.Grind.instInhabitedInjectiveTheorem.default : InjectiveTheorem

Equations

• Lean.Meta.Grind.instInhabitedInjectiveTheorem.default = { levelParams := default, proof := default, symbols := default, origin := default }

instance Lean.Meta.Grind.instTheoremLikeInjectiveTheorem : TheoremLike InjectiveTheorem

Equations

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

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

def Lean.Meta.Grind.instInhabitedEntry.default : Entry

Equations

• Lean.Meta.Grind.instInhabitedEntry.default = Lean.Meta.Grind.Entry.ext default

instance Lean.Meta.Grind.instInhabitedEntry : Inhabited Entry

Equations

• Lean.Meta.Grind.instInhabitedEntry = { default := Lean.Meta.Grind.instInhabitedEntry.default }

structure Lean.Meta.Grind.ExtensionState : Type

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

instance Lean.Meta.Grind.instInhabitedExtensionState : Inhabited ExtensionState

Equations

• Lean.Meta.Grind.instInhabitedExtensionState = { default := Lean.Meta.Grind.instInhabitedExtensionState.default }

def Lean.Meta.Grind.instInhabitedExtensionState.default : ExtensionState

Equations

• Lean.Meta.Grind.instInhabitedExtensionState.default = { casesTypes := default, extThms := default, funCC := default, ematch := default, inj := default }

@[reducible, inline]

abbrev Lean.Meta.Grind.Extension : Type

Equations

• Lean.Meta.Grind.Extension = Lean.SimpleScopedEnvExtension Lean.Meta.Grind.Entry Lean.Meta.Grind.ExtensionState

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

Equations

• s.addEntry (Lean.Meta.Grind.Entry.cases declName eager) = { casesTypes := s.casesTypes.insert declName eager, extThms := s.extThms, funCC := s.funCC, ematch := s.ematch, inj := s.inj }
• s.addEntry (Lean.Meta.Grind.Entry.ext declName) = { casesTypes := s.casesTypes, extThms := Lean.PersistentHashSet.insert s.extThms declName, funCC := s.funCC, ematch := s.ematch, inj := s.inj }
• s.addEntry (Lean.Meta.Grind.Entry.funCC declName) = { casesTypes := s.casesTypes, extThms := s.extThms, funCC := s.funCC.insert declName, ematch := s.ematch, inj := s.inj }
• s.addEntry (Lean.Meta.Grind.Entry.ematch thm) = { casesTypes := s.casesTypes, extThms := s.extThms, funCC := s.funCC, ematch := s.ematch.insert thm, inj := s.inj }
• s.addEntry (Lean.Meta.Grind.Entry.inj thm) = { casesTypes := s.casesTypes, extThms := s.extThms, funCC := s.funCC, ematch := s.ematch, inj := s.inj.insert thm }

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

Equations

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

@[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.

Equations

• Lean.Meta.Grind.ExtensionStateArray = Array Lean.Meta.Grind.ExtensionState

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

Equations

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