~/jendhub

def ne_from

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:189

import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

189def ne_from(+d: Nat, +e: Nat, same: {e == d : Nat}, differ: {Nat.is_eq(d, e) == False{} : Bool}) -> Empty:
190  Arith.clash(Equal.trans(Bool, False{}, Nat.is_eq(d, e), True{}, Equal.sym(Bool, Nat.is_eq(d, e), False{}, differ),
191    %Equal.sym(Nat, e, d, same) : {Nat.is_eq(d, _) == True{} : Bool}
192    Arith.eq_refl(d)))

Uses (8)

Used by (1)