Commit 2021-11-30 17:06 ceae8916
View on Github →refactor(Data/Int): move Int notation to separate file (#113)
- Rename
one_succ_zero
->one_eq_succ_zero
- Declare
ℤ
notation in init - Minimize some imports
refactor(Data/Int): move Int notation to separate file (#113)
one_succ_zero
-> one_eq_succ_zero
ℤ
notation in init