def Clamp.ge

bend-collections-laws-crypto@1.0.0.0 · spec/math/natural.bend:290

import Base

290def Clamp.ge(+x: Nat, +lo: Nat, +hi: Nat, +h: {Nat.is_le(lo, hi) == True{} : Bool}) -> Type:
291  {Nat.is_le(lo, Nat.min(Nat.max(x, lo), hi)) == True{} : Bool}