structure HexGraphIsoTheory.AutTactic.Config : Type

Resource limits for one graph_aut call.

• maxSearchNodes : ℕ

  Search nodes allowed for each canonical-key certificate.

• maxCertRecords : ℕ

  Total canonical-certificate records allowed in the graph certificate.

• maxChunkWork : ℕ

  Estimated kernel work in each permutation-group checker chunk.

def HexGraphIsoTheory.AutTactic.elabGraphAutConfig (cfg : Lean.Syntax) (init : Config := { }) (logExceptions : Bool := true) : Lean.Elab.Tactic.TacticM Config

Equations

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

def HexGraphIsoTheory.AutTactic.graphAut : Lean.ParserDescr

Prove the order or explicit generator description of the automorphism group of a closed graph by kernel-checked certificates.

Equations

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

def HexGraphIsoTheory.AutTactic.evalGraphAut : Lean.Elab.Tactic.Tactic

Equations

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