Source/Reference

BinaryFloatModel

reference/numeric/BinaryFloatModel.alpha

467 lines54 declarations18.3 KiBSHA-256 cc13dd71cf68

def · lines 128–140

modelSignedScale

Full file
128def modelSignedScale =
129  (lambda unrestricted value : (family ModelSigned) .
130    (lambda unrestricted factor : Nat .
131      (eliminate
132        ModelSigned
133        (lambda unrestricted current : (family ModelSigned) . (family ModelSigned))
134        value
135        (branch
136          ModelSignedOf
137          sign
138          magnitude
139          .
140          (constructor ModelSigned ModelSignedOf sign (nat-multiply magnitude factor))))))

The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.