Commit 2023-03-31 13:00 98f40c35
View on Github →refactor: Refactor coercions in Data.Num.Basic
(#2780)
This PR:
- gives the coercions
coe
attributes. - replace
coeTC
withcoeHTCT
, otherwise coercions get complicated as shown.
variable (p : PosNum)
example : ℤ := p -- ↑↑p, we want ↑p.