def Clamp.id

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

import Base

296def Clamp.id(+x: Nat, +lo: Nat, +hi: Nat, +h1: {Nat.is_le(lo, x) == True{} : Bool}, +h2: {Nat.is_le(x, hi) == True{} : Bool}) -> Type:
297  {Nat.min(Nat.max(x, lo), hi) == x : Nat}