Dev/Smoke/ReachabilityWrapper/Contract.lean
| 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 |