type Outside

stelliferous@0.0.2.0 · proofs/nat_interval.bend:22

import Base

22# A query lies strictly before or at/after the end of a half-open interval.
23type Outside<-start: Nat,-length: Nat,-query: Nat> is Data:
24  Before{bound: {Nat.is_lt(query,start) == True{} : Bool}}
25  After{bound: {Nat.is_le(Nat.add(start,length),query) == True{} : Bool}}