def nat_clash
bendtorch-core@0.1.0.0 · src/tensor/axis_algebra.bend:186
import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as AxisAlgebra
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
186def nat_clash(+a: Nat, +b: Nat, equal: {a == b : Nat}, different: {False{} == Nat.is_eq(a, b) : Bool}) -> Empty:
187 Shape.clash(Equal.trans(Bool, True{}, Nat.is_eq(a, b), False{},
188 Equal.trans(Bool, True{}, Nat.is_eq(b, b), Nat.is_eq(a, b), Equal.sym(Bool, Nat.is_eq(b, b), True{}, Arith.eq_refl(b)),
189 Equal.cong(Nat, Bool, n => Nat.is_eq(n, b), b, a, Equal.sym(Nat, a, b, equal))),
190 Equal.sym(Bool, False{}, Nat.is_eq(a, b), different)))