Dev.Smoke.ReachabilityWrapper
Definition
Smoke-test definition. Let \(G\) be a finite simple graph on a linearly ordered vertex set \(V\), let \(r \in \mathbb{N}\), and let \(v \in V\). Define \(\mathrm{smokeReach}(G, r, v)\) to equal the strong \(r\)-reachability set from Definition ColoringNumbers. This entry exists only to exercise cross-package imports from the dev library into the catalog.
Review notes
Smoke test entry validating cross-package imports from the dev
library (Dev.*) into the archival catalog (Catalog.*).
The definition is intentionally a thin wrapper around
Catalog.Sparsity.ColoringNumbers.SReach, so Contract and Full
are definitionally identical.
Dev/Smoke/ReachabilityWrapper/Contract.lean (full)
| 1 | import Catalog.Sparsity.ColoringNumbers.Contract |
| 2 | |
| 3 | namespace Dev.Smoke.ReachabilityWrapper |
| 4 | |
| 5 | open Catalog.Sparsity.ColoringNumbers |
| 6 | |
| 7 | variable {V : Type*} [DecidableEq V] [Fintype V] [LinearOrder V] |
| 8 | |
| 9 | /-- Smoke-test wrapper around `SReach` from |
| 10 | `Catalog.Sparsity.ColoringNumbers`. -/ |
| 11 | def smokeReach (G : SimpleGraph V) (r : ℕ) (v : V) : Set V := |
| 12 | SReach G r v |
| 13 | |
| 14 | end Dev.Smoke.ReachabilityWrapper |
| 15 |
Dependencies
Statement