def pair_fits

bendtorch-core@0.1.0.0 · src/shape/coordinate_proofs.bend:200

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

200def pair_fits(+shape: Shape.Shape, +first: U32, +second: U32, +x: U32, +y: U32,
201  dimensions: {Shape.dimensions(shape) == [first, second] : List<&2, U32>},
202  first_inside: {Nat.is_lt(U32.to_nat(x), U32.to_nat(first)) == True{} : Bool},
203  second_inside: {Nat.is_lt(U32.to_nat(y), U32.to_nat(second)) == True{} : Bool}) -> Fits(Shape.extents(shape), [U32.to_nat(x), U32.to_nat(y)]):
204  fits_of(Shape.extents(shape), [U32.to_nat(x), U32.to_nat(y)],
205    %Equal.sym(List<&2, U32>, Shape.dimensions(shape), [first, second], dimensions) :
206      {True{} == Shape.fit(Shape.naturals(_), [U32.to_nat(x), U32.to_nat(y)]) : Bool}
207    %Equal.sym(Bool, Nat.is_lt(U32.to_nat(x), U32.to_nat(first)), True{}, first_inside) :
208      {True{} == Bool.and(_, Bool.and(Nat.is_lt(U32.to_nat(y), U32.to_nat(second)), True{})) : Bool}
209    %Equal.sym(Bool, Nat.is_lt(U32.to_nat(y), U32.to_nat(second)), True{}, second_inside) :
210      {True{} == Bool.and(True{}, Bool.and(_, True{})) : Bool}
211    {==})