def
Hex.GraphIso.Nauty.Sparse.canonContract
{n k : Nat}
(G : Sparse.Colored n k)
:
Generic.Contract (State n) n
Actual native frame and canonical-reference effects have the same entry conditions, including truncated calls and arbitrary return targets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.canon_node
{n k : Nat}
(G : Sparse.Colored n k)
(hn : 0 < n)
(tcLevel : Nat)
{fuel : Nat}
{next : Generic.SweepFn (State n) n}
(hnext : (canonContract G).sweepValid fuel (n + 1) next)
(first : Bool)
(level numcells : Nat)
(st : State n)
(hl : 1 ≤ level)
(h : NodeInv G level numcells st)
:
CanonOut level st (Generic.nodeStep (Graph.ofGraph G.graph) tcLevel next first level numcells st).snd
Native node preparation and leaf actions preserve canonical provenance; an installed reference belongs to this node's actual cached refinement.