~/jendhub

def shifted_bound

stelliferous@0.0.2.0 · proofs/u32_division.bend:40

import stelliferous@0.0.2.0/proofs/u32_division.bend as U32Division
import Base

40def shifted_bound(+s: U32,+value: Nat,+cap: U32,e: {U32.to_nat(s) == value : Nat},h: {Nat.is_le(value,
41      U32.to_nat(cap)) == True{} : Bool}) -> {Nat.is_le(U32.to_nat(s),U32.to_nat(cap)) == True{} : Bool}:
42  %Equal.sym(Nat,U32.to_nat(s),value,e) : {Nat.is_le(_,U32.to_nat(cap)) == True{} : Bool}
43  h

Uses (6)

Used by (1)