~/jendhub

def half_double

bendtorch-core@0.1.0.0 · src/tensor/word_injective.bend:22

import bendtorch-core@0.1.0.0/src/tensor/word_injective.bend as WordInjective
import Base

22def half_double(+number: Nat) -> {half(Nat.double(number)) == number : Nat}:
23  match number:
24    case 0n:
25      {==}
26    case 1n+p:
27      Equal.cong(Nat, Nat, n => 1n+n, half(Nat.double(p)), p, half_double(p))

Uses (4)

Used by (1)