def Float64.lt_one
import bend-collections-laws-math@1.0.0.0/proofs/math/random/proof_float.bend as ProofFloatimport Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
import bend-collections-laws-math@1.0.0.0/spec/math/random.bend as SRM
import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as FL
20def Float64.lt_one(+x: W.U64) -> SRM.Float64.lt_one(x):
21 FL.lt_one(x)
Uses (3)
Used by (0)
No other definition uses this definition.