~/bend-docscommunity

proofs/nat_interval.bend checks

raw source on the hub · import stelliferous@0.0.2.0/proofs/nat_interval.bend as Nat_interval

5 imports
import Base
import ./nat_order.bend as Order
import ./nat_to_u32_bounds.bend as Bounds
import ./natural_addition.bend as Addition
import ./nat_extrema.bend as Extrema

Types

type Outside source · line 23 · raw

@-start:Nat -> @-length:Nat -> @-query:Nat -> Data

A query lies strictly before or at/after the end of a half-open interval.

Definitions

def shifted_inside source · line 7 · raw

@+begin:Nat -> @+end:Nat -> @+query:Nat -> @+lower:{Nat.is_le(begin, query) == True{} : Bool} -> @+upper:{Nat.is_lt(query, end) == True{} : Bool} -> {Nat.is_lt(Nat.sub(query, begin), Nat.sub(end, begin)) == True{} : Bool}

def shifted_span source · line 14 · raw

@+first:Nat -> @+rows:Nat -> @+begin:Nat -> @+end:Nat -> @lower:{Nat.is_le(first, begin) == True{} : Bool} -> @ordered:{Nat.is_le(begin, end) == True{} : Bool} -> @upper:{Nat.is_le(end, Nat.add(first, rows)) == True{} : Bool} -> {Nat.is_le(Nat.add(Nat.sub(begin, first), Nat.sub(end, begin)), rows) == True{} : Bool}

def outside_head source · line 27 · raw

@+start:Nat -> @+remaining:Nat -> @+query:Nat -> @outside:Outside<start, 1n+remaining, query> -> {Nat.is_eq(query, start) == False{} : Bool}

def outside_tail source · line 35 · raw

@+start:Nat -> @+remaining:Nat -> @+query:Nat -> @outside:Outside<start, 1n+remaining, query> -> Outside<1n+start, remaining, query>