def add_zero

bendtorch-core@0.1.0.0 · src/tensor/word_conversion.bend:203

import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion

import Base

203def add_zero(+number: Nat) -> {Nat.add(number, 0n) == number : Nat}:
204  match number:
205    case 0n:
206      {==}
207    case 1n+p:
208      Equal.cong(Nat, Nat, n => 1n+n, Nat.add(p, 0n), p, add_zero(p))

Uses (3)

Used by (8)