← Mathematical handbook

def Lean.Elab.Tactic.Grind.isGrindAnnotatedModule (env : Environment) (modIdx : ModuleIdx) : Bool

Check if a module has been marked as grind-annotated.

Equations

• Lean.Elab.Tactic.Grind.isGrindAnnotatedModule env modIdx = (Lean.Elab.Tactic.Grind.grindAnnotatedExt✝.getState env).contains env.header.moduleNames[modIdx.toNat]!