def natural_equal_true

bendtorch-core@0.1.0.0 · src/tensor/permutation_mapping.bend:156

import bendtorch-core@0.1.0.0/src/tensor/permutation_mapping.bend as PermutationMapping

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

156def natural_equal_true(+left: Nat, +right: Nat, same: {left == right : Nat}) -> {Nat.is_eq(left, right) == True{} : Bool}:
157  %same : {Nat.is_eq(left, _) == True{} : Bool}
158  Arith.eq_refl(left)

Uses (4)

Used by (3)