Dev smoke tests
Main results: ReachabilityWrapper
1Overview
statement dependency
proof dependency
All Entries
2 Main Results
ReachabilityWrapper
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.
| 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 |