def unit_nat

bendtorch-core@0.1.0.0 · src/storage/arith.bend:406

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model

406def unit_nat(+m: Nat, +k: Nat, h: {Nat.is_lt(k, m) == True{} : Bool}) -> {Model.capacity(k) == Word.to_nat(m, unit(m, k)) : Nat}:
407  match m:
408    case 0n:
409      match k:
410        case 0n:
411          Empty.absurd({1n == 0n : Nat}, clash(h))
412        case 1n+r:
413          Empty.absurd({Model.capacity(1n+r) == 0n : Nat}, clash(h))
414    case 1n+q:
415      match k:
416        case 0n:
417          %zero_nat(q) : {1n == 1n+Nat.double(_) : Nat}
418          {==}
419        case 1n+r:
420          %unit_nat(q, r, h) : {Model.capacity(1n+r) == Nat.double(_) : Nat}
421          double_self(Model.capacity(r))