Fractional typeclass.
A typeclass for fractional assertions, that is assertions that depend on a fraction and that can be split.
This is used to derive generically a few other instances for framing , destructing, combining and spliting assertions of sums of fractions. I found it usefull when doing fraction-heavy proofs in LambdaRust.
The Right Way To Do It would be to use a typeclass over the predicate itself. Unfortunately, the unification algorithm of typeclasses is not powerful enough to do the right beta-expansion that would expose the predicate applied to some fraction. Instead, the Fractional type class has as parameters both the predicate and the applied form that can be directly unified with the fractured assertion. Not very pretty.
I wonder whether I should split this into two type classes: the first one would depend only on the predicate and would actually state the fractionality of it, and the second would do the beta-expansion job. What do you think?