Commit 2023-03-31 13:00 98f40c35

View on Github →

refactor: Refactor coercions in Data.Num.Basic (#2780) This PR:

  1. gives the coercions coe attributes.
  2. replace coeTC with coeHTCT, otherwise coercions get complicated as shown.
variable (p : PosNum)
example : ℤ := p -- ↑↑p, we want ↑p.

Estimated changes

modified def castNum
modified def castPosNum
modified def castZNum