Arith.unit_nat: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
Lines 406-421 of bendtorch-core@0.1.0.0/src/storage/arith.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&start_line=406&end_line=421

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

def 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}:
  match m:
    case 0n:
      match k:
        case 0n:
          Empty.absurd({1n == 0n : Nat}, clash(h))
        case 1n+r:
          Empty.absurd({Model.capacity(1n+r) == 0n : Nat}, clash(h))
    case 1n+q:
      match k:
        case 0n:
          %zero_nat(q) : {1n == 1n+Nat.double(_) : Nat}
          {==}
        case 1n+r:
          %unit_nat(q, r, h) : {Model.capacity(1n+r) == Nat.double(_) : Nat}
          double_self(Model.capacity(r))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=double_self
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=zero_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=capacity