def Hex.SieveElab.rebuildPrimeTable : Lean.ParserDescr

Generate the committed table and its verification block; see the module docstring.

Equations

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

def Hex.SieveElab.elabRebuildPrimeTable : Lean.Elab.Command.CommandElab

Elaborate #rebuild_primeTable into the generated table and proof block.

Equations

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