def counted_is

bendtorch-core@0.1.0.0 · src/tensor/gather_PROOF.bend:119

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/gather.bend as Gather
import bendtorch-core@0.1.0.0/src/tensor/gather_LAWS.bend as Laws

119# The entry count rewrites to its value.
120def counted_is(+entries: List<&2, U32>, +index: Shape.Shape, +value: Bool,
121  given: {Nat.is_eq(Laws.length(entries), Shape.elements(index)) == value : Bool}) ->
122  {value == Nat.is_eq(Gather.count(entries), Shape.elements(index)) : Bool}:
123  Equal.sym(Bool, Nat.is_eq(Gather.count(entries), Shape.elements(index)), value,
124    Equal.trans(Bool, Nat.is_eq(Gather.count(entries), Shape.elements(index)), Nat.is_eq(Laws.length(entries), Shape.elements(index)),
125      value,
126      Equal.cong(Nat, Bool, n => Nat.is_eq(n, Shape.elements(index)), Gather.count(entries), Laws.length(entries), count_length(entries)),
127      given))