def parity_clash
bendtorch-core@0.1.0.0 · src/tensor/word_injective.bend:49
import bendtorch-core@0.1.0.0/src/tensor/word_injective.bend as WordInjective
import Base
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
49def parity_clash(+left: Nat, +right: Nat, equal: {Nat.double(left) == 1n+Nat.double(right) : Nat}) -> Empty:
50 Lifecycle.false_true(Equal.trans(Bool, True{}, even(Nat.double(left)), False{},
51 Equal.sym(Bool, even(Nat.double(left)), True{}, even_double(left)),
52 Equal.trans(Bool, even(Nat.double(left)), even(1n+Nat.double(right)), False{},
53 Equal.cong(Nat, Bool, n => even(n), Nat.double(left), 1n+Nat.double(right), equal), even_successor_double(right))))