Integers that play nice with typechecking#56

Draft

ohad wants to merge 7 commits intomainfrom integers

+590

Commits on Nov 26, 2021

Start thinking formalising integers in a way that plays well with type-checking
Ohad Kammar
committed
Continue to prove stuff
Ohad Kammar
committed
Define the additive monoid structure on the integers
Ohad Kammar
committed
Give an inductive representation of the integers
Ohad Kammar
committed
Prove a representation theorem for the quotient
Ohad Kammar
committed

Commits on Nov 27, 2021

Add a stub group frexlet
Ohad Kammar
committed
Transport group structure to inductive integers
Ohad Kammar
committed