rat.bend checks
raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/rat.bend as Rat
2 imports
import Base import ./math.bend as Math
Laws
law radd_1_2_1_3 provedsource · line 113 · raw
{radd(mk_rat(False{}, 1, 2), mk_rat(False{}, 1, 3)) == mk_rat(False{}, 5, 6) : Rat}
law rmul_2_3_3_4 provedsource · line 120 · raw
{rmul(mk_rat(False{}, 2, 3), mk_rat(False{}, 3, 4)) == mk_rat(False{}, 1, 2) : Rat}
law rsub_3_4_1_4 provedsource · line 127 · raw
{rsub(mk_rat(False{}, 3, 4), mk_rat(False{}, 1, 4)) == mk_rat(False{}, 1, 2) : Rat}
law req_sym_1_2_1_3 provedsource · line 134 · raw
{req(mk_rat(False{}, 1, 2), mk_rat(False{}, 1, 3)) == req(mk_rat(False{}, 1, 3), mk_rat(False{}, 1, 2)) : Bool}
law rdiv_1_2_1_4 provedsource · line 141 · raw
{rdiv(mk_rat(False{}, 1, 2), mk_rat(False{}, 1, 4)) == mk_rat(False{}, 2, 1) : Rat}
Types
type Rat source · line 32 · raw
Data
R@neg:Bool -> @num:U32 -> @den:U32 -> Rat
Definitions
def mk_rat source · line 36 · raw
@neg:Bool -> @+num:U32 -> @+den:U32 -> Rat
mk_rat: reduce by gcd, canonicalize zero. Straight-line, no match.
def radd source · line 49 · raw
@a:Rat -> @b:Rat -> Rat
radd: signed addition, straight-line picks (no match on computed). Same sign: mk_rat(s1, p1 + p2, den). Different signs: the larger magnitude wins (cmp on the cross products, exact absent wrap); a tie is zero. Follows the pyval int_add_raw shape.
def rsub source · line 67 · raw
@a:Rat -> @b:Rat -> Rat
rsub: negate b's sign, then radd (rebuild is a constructor, not a match on computed; radd matches on its own parameters).
def rmul source · line 73 · raw
@a:Rat -> @b:Rat -> Rat
rmul: xor signs, multiply through, normalize.
def rdiv source · line 79 · raw
@a:Rat -> @b:Rat -> Rat
rdiv: invert b (swap num/den; requires b's num != 0), then rmul.
def req source · line 85 · raw
@a:Rat -> @b:Rat -> Bool
req: decidable equality (cross-multiply + both-zero collapse).
def neg_of source · line 95 · raw
@r:Rat -> Bool
def num_of source · line 100 · raw
@r:Rat -> U32
def den_of source · line 105 · raw
@r:Rat -> U32