def outside_tail

stelliferous@0.0.2.0 · proofs/nat_interval.bend:35

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds

35def outside_tail(+start: Nat,+remaining: Nat,+query: Nat,outside: Outside<start,1n+remaining,query>) -> Outside<1n+start,remaining,query>:
36  match outside:
37    case Before{bound}: Before{Order.lt_succ(query,start,Bounds.strict_le(query,start,bound))}
38    case After{bound}: After{Order.advance_room(start,remaining,query,bound)}