Commit 2022-02-01 18:42 cc9b9f34

refactor: remove numeric (#177) This removes the Numeric parent for Semiring which was used for both coercions and numerals, and replaces it by a low-priority instance for OfNat on Semiring. The coercion from Nat to R is removed. Numerals are now implemented using Nat.cast. As Sebastian has noted, to avoid diamonds for numerals it suffices that Nat.cast n and (n : R) are definitionally equal for every n : Nat. It is not necessary that (Nat.cast ∙) and (∙ : R) are definitionally equal as functions (and after this PR they are not, for most rings). Similarly, Nat.cast is carefully defined so that both 0 = 0 and 1 = 1 are true definitionally in any ring. The setup still has a couple of downsides:

1. OfNat.ofNat must never be applied to anything except concrete natural numbers (or we get diamonds).
2. (123456 : R) is a massive performance issue when executing in the VM. :-/ (Which is not entirely true, in reality it fails quickly due to a stack overflow.) We do not register Nat.cast as a coercion because of the performance issues.