lean/SpectreKnot.lean
33 lines · no declarations · on GitHub ·
The root of the library: it imports the files of the formalisation.
← SpectreKnot/Data/Level2.leanThe Lean formalisation →
All 39 files, and the declarations of this one
1import SpectreKnot.Basic
2import SpectreKnot.Data.Pattern
3import SpectreKnot.Lengths
4import SpectreKnot.Strands
5import SpectreKnot.Box
6import SpectreKnot.Zigzag
7import SpectreKnot.Gluing
8import SpectreKnot.Compose
9import SpectreKnot.CompFull
10import SpectreKnot.Subdivide
11import SpectreKnot.Lens
12import SpectreKnot.Move
13import SpectreKnot.Signature
14import SpectreKnot.ParentRim
15import SpectreKnot.CompSig
16import SpectreKnot.Parity
17import SpectreKnot.Statement
18import SpectreKnot.PatchSig
19import SpectreKnot.ComposeTiles
20import SpectreKnot.Reverse
21import SpectreKnot.Bridge
22import SpectreKnot.ParentSig
23import SpectreKnot.ProofA
24import SpectreKnot.NewWalk
25import SpectreKnot.StepMap
26import SpectreKnot.Linked
27import SpectreKnot.NestStep
28import SpectreKnot.ProofB
29import SpectreKnot.ProofStrand
30import SpectreKnot.ProofChain
31import SpectreKnot.ProofExact
32import SpectreKnot.Turn
33import SpectreKnot.ProofGrand