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 := { casesMap := default } }

structure Lean.Meta.Grind.CasesEntry : Type

• declName : Name
• eager : Bool

instance Lean.Meta.Grind.instInhabitedCasesEntry : Inhabited CasesEntry

Equations

• Lean.Meta.Grind.instInhabitedCasesEntry = { default := { declName := default, eager := default } }

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?

Equations

• Lean.Meta.Grind.isBuiltinEagerCases declName = Lean.Meta.Grind.builtinEagerCases✝.contains declName

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

Returns true if s contains a declName.

Equations

• s.contains declName = Lean.PersistentHashMap.contains s.casesMap declName

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

Removes the given declaration from s.

Equations

• s.erase declName = { casesMap := Lean.PersistentHashMap.erase s.casesMap declName }

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 }

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

Equations

• s.find? declName = Lean.PersistentHashMap.find? s.casesMap declName

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

Equations

• s.isEagerSplit declName = ((Lean.PersistentHashMap.find? s.casesMap declName).getD false || Lean.Meta.Grind.isBuiltinEagerCases declName)

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

Equations

• s.isSplit declName = ((Lean.PersistentHashMap.find? s.casesMap declName).isSome || Lean.Meta.Grind.isBuiltinEagerCases declName)

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

def Lean.Meta.Grind.resetCasesExt : CoreM Unit

Equations

• Lean.Meta.Grind.resetCasesExt = Lean.modifyEnv fun (env : Lean.Environment) => Lean.ScopedEnvExtension.modifyState Lean.Meta.Grind.casesExt env fun (x : Lean.Meta.Grind.CasesTypes) => { }

def Lean.Meta.Grind.getCasesTypes : CoreM CasesTypes

Equations

• Lean.Meta.Grind.getCasesTypes = do let __do_lift ← Lean.getEnv pure (Lean.ScopedEnvExtension.getState Lean.Meta.Grind.casesExt __do_lift)

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

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

Equations

• Lean.Meta.Grind.isSplit declName = do let __do_lift ← Lean.Meta.Grind.getCasesTypes pure (__do_lift.isSplit declName)

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

Equations

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

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

Equations

• Lean.Meta.Grind.isCasesAttrCandidate declName eager = do let __do_lift ← Lean.Meta.Grind.isCasesAttrCandidate? declName eager pure __do_lift.isSome

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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