int.md

types.int

The integers. Note: most of these 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).

• basic : the integers, with basic operations
• order : order on the integers
• hott : facts about the integers specific to the HoTT library