To build, run make
at the base level of the project directory.
The overlapping pattern matching construction (theorem 1 from the draft)
is found in src/Sublocale.v
in the section called Pattern
.
The computation rule for splitting points with open covers is found in
src/FrameC.v
and has the identifier point_cov_top
.
This code was essentially extracted from a much larger codebase that provides various bits of functionality for programming with spaces, including many constructions of formal topology and (predicative) locale theory.