lean/TestsSlow.lean
19 lines · no declarations · on GitHub ·
Slower tests: the level-5 entries of the paper's Table 5 and of the chain of its §10 (about 6 minutes), and the conclusion of the parity lemma (the paper's Prop 7.4) at level 2, computed directly. Run with ./build.sh --slow.
← Tests.leanSpectreKnot/Data/Pattern.lean →
All 39 files, and the declarations of this one
1/-
2Slower tests: the level-5 entries of the paper's Table 5 and of the chain of its §10 (about 6 minutes), and the
3conclusion of the parity lemma (the paper's Prop 7.4) at level 2, computed directly.
4Run with `./build.sh --slow`.
5-/
8open SpectreKnot Compose StatementTests
10-- N_1 and N_2 lie on a single strand of N_5 (Table 5: k = 4 for b = 1, k = 3 for b = 2)
11#guard [nestCount 1 4, nestCount 2 3] == [1, 1]
13-- along the chain of §10, X_1 still lies on three strands of X_5
14#guard chainCount 1 4 == 3
16-- the parity lemma (Prop 7.4) at level 2, computed directly (it is proved for every level `m ≥ 1`)
18 let C := Comp.ofPattern T (letterLen 2) (dOff 2) ω
19 C.check ω