AlphaGitHub
Source/Reference

Float32Model

reference/numeric/Float32Model.alpha

410 lines71 declarations23.3 KiBSHA-256 dd3156cf3c08
Download exact fileView at revisionf5034773ad4bb52133

def · lines 299–307

modelF32Less

Full file
299def modelF32Less =
300  (lambda unrestricted a : Nat . (lambda unrestricted b : Nat .
301    (specSelect (modelOr (modelIsNaN a) (modelIsNaN b))
302      0
303      (specSelect (modelAnd (modelIsZero a) (modelIsZero b))
304        0
305        (specSelect (modelSign a)
306          (specSelect (modelSign b) (nat-less-than (modelOrderKey b) (modelOrderKey a)) 1)
307          (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.