def even_double

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

import Base

29def even_double(+number: Nat) -> {even(Nat.double(number)) == True{} : Bool}:
30  match number:
31    case 0n:
32      {==}
33    case 1n+p:
34      even_double(p)