~amiloradovsky/symbolic-dynamics

.build.yml: continuous integration for SourceHut
Topological: uniform structure on topological groups
Dynamical: discrete-time topological dynamical systems

Previously known as Miscellaneous, but it wasn't anymore.
Pattern_Sets, Concatenation: separate modules from Patterns
Metric_Space: separate module for some metric properties
Decidable: module for dealing with e.g. the finiteness
Language: separate module for languages as pattern-sets
Patterns_US: module for the uniform structure on patterns
Local_Rule: separate module for the anchored local rule
Prodiscrete: separete module for the topology-related stuff
Patterns: extended the equivalence proof (LR = UC) to subsets
55af6384 — Pierre Guillon 11 months ago
adapted roadmap
Patterns: generalized the definition of entourage a little
Patterns: optimized the local rule and uniformity definitions

They actually do not depend on the pro-discrete topology anyhow.
These may & should be formulated directly with the configurations,
so no conversion to/from the point-set is needed anymore.

Thus moved the topology-related stuff to the end of the module.
Patterns: optimized the definition of an anchored pattern
Patterns: proved that the finite supports are decidable
Patterns: the local rule is equivalent to uniform continuity*

* modulo the simplifications (only full shift, not any sub-shift),
  and also couple reasonable assumptions (e.g. decidable supports)
Uniform: fixed / clarified the definition of uniform continuity
Added a copying information (LGPL 2.1); improved .gitignore

Same terms as of the dependencies: Coq itself and the topology library.
Patterns: broke up the uniformity proof into multiple lemmas
Next