structure Lean.Meta.Grind.CasesTypes : Type

Types that grind will case-split on.

• casesMap : PHashMap Name Bool

instance Lean.Meta.Grind.instInhabitedCasesTypes : Inhabited CasesTypes

structure Lean.Meta.Grind.CasesEntry : Type

• declName : Name
• eager : Bool

instance Lean.Meta.Grind.instInhabitedCasesEntry : Inhabited CasesEntry

def Lean.Meta.Grind.isBuiltinEagerCases (declName : Name) : Bool

Returns true if declName is the name of inductive type/predicate that even grind only case splits on. Remark: we added support for them to reduce the noise in the tactic generated by grind?

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

Returns true if s contains a declName.

def Lean.Meta.Grind.CasesTypes.erase (s : CasesTypes) (declName : Name) : CasesTypes

Removes the given declaration from s.

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

def Lean.Meta.Grind.CasesTypes.find? (s : CasesTypes) (declName : Name) : Option Bool

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

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

opaque Lean.Meta.Grind.casesExt : SimpleScopedEnvExtension CasesEntry CasesTypes

def Lean.Meta.Grind.resetCasesExt : CoreM Unit

def Lean.Meta.Grind.getCasesTypes : CoreM CasesTypes

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

Returns true is declName is a builtin split or has been tagged with [grind] attribute.

def Lean.Meta.Grind.isCasesAttrCandidate? (declName : Name) (eager : Bool) : CoreM (Option Name)

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

def Lean.Meta.Grind.isCasesAttrPredicateCandidate? (declName : Name) (eager : Bool) : MetaM (Option InductiveVal)

def Lean.Meta.Grind.validateCasesAttr (declName : Name) (eager : Bool) : CoreM Unit

def Lean.Meta.Grind.addCasesAttr (declName : Name) (eager : Bool) (attrKind : AttributeKind) : CoreM Unit

def Lean.Meta.Grind.CasesTypes.eraseDecl (s : CasesTypes) (declName : Name) : CoreM CasesTypes

def Lean.Meta.Grind.ensureNotBuiltinCases (declName : Name) : CoreM Unit

def Lean.Meta.Grind.eraseCasesAttr (declName : Name) : CoreM Unit

def Lean.Meta.Grind.cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId)

The grind tactic includes an auxiliary cases tactic that is not intended for direct use by users. This method implements it. This tactic is automatically applied when introducing local declarations with a type tagged with [grind_cases]. It is also used for "case-splitting" on terms during the search.

It differs from the user-facing Lean cases tactic in the following ways:

• It avoids unnecessary revert and intro operations.

• It does not introduce new local declarations for each minor premise. Instead, the grind tactic preprocessor is responsible for introducing them.

• If the major premise type is an indexed family, auxiliary declarations and (heterogeneous) equalities are introduced. However, these equalities are not resolved using unifyEqs. Instead, the grind tactic employs union-find and congruence closure to process these auxiliary equalities. This approach avoids applying substitution to propositions that have already been internalized by grind.

def Lean.Meta.Grind.cases.throwInductiveExpected (mvarId : MVarId) (e : Expr) {α : Type} (type : Expr) : MetaM α