def cap_nat

bendtorch-core@0.1.0.0 · src/storage/route.bend:265

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/size.bend as Size
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

265def cap_nat(+d: Nat, +h: {Nat.is_le(d, 20n) == True{} : Bool}) -> {Model.capacity(d) == U32.to_nat(Size.capacity(d)) : Nat}:
266  %cap_unit(d, h) : {Model.capacity(d) == U32.to_nat(_) : Nat}
267  Arith.unit_nat(32n, d, Arith.lt_le_trans(d, 21n, 32n, Arith.lt_succ(d, 20n, h), {==}))