The following files are ported from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also script/port.pl).
- priority : priority for algebraic operations
- relation
- binary : binary operations
- order
- lattice
- group
- ring
- ordered_group
- ordered_ring
- field
- ordered_field
- bundled : bundled versions of the algebraic structures
- homomorphism
- group_power (depends on files in nat and int)
Files which are not ported from the standard library:
- inf_group : algebraic structures which are not assumes to be sets. No higher coherences are assumed. Truncated algebraic structures extend these structures with the assumption that they are sets.
- inf_group_theory : Some very basic group theory using InfGroups
- group_theory : Basic theorems about group homomorphisms and isomorphisms
- trunc_group : truncate an infinity-group to a group
- homotopy_group : homotopy groups of a pointed type
- e_closure : the type of words formed by a relation, or paths in a graph.
- graph : definition and operations on paths in a graph.
Subfolders (not ported):
- category : Category Theory