AlphaGitHub
Source/Reference

Float32Model

reference/numeric/Float32Model.alpha

304 lines61 declarations17.2 KiBSHA-256 421f33839d13
Download exact fileView at revisionbcc11a4e7647d31628

def · lines 193–201

modelF32Less

Full file
193def modelF32Less =
194  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
195    (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
196      0
197      (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
198        0
199        (specSelect (modelSign a)
200          (specSelect (modelSign b) (nat-less-than (modelOrderKey b) (modelOrderKey a)) 1)
201          (specSelect (modelSign b) 0 (nat-less-than (modelOrderKey a) (modelOrderKey b))))))))

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.