def zero_nat

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

import Base

398def zero_nat(+q: Nat) -> {0n == Word.to_nat(q, Word.zero(q)) : Nat}:
399  match q:
400    case 0n:
401      {==}
402    case 1n+p:
403      %zero_nat(p) : {0n == Nat.double(_) : Nat}
404      {==}