def horner_fits
bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:132
import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
132def horner_fits(+shape: Shape.Shape, +values: List<&2, U32>, +fits: Coordinates.Fits(Shape.extents(shape), Shape.naturals(values))) -> {Shape.horner(Shape.dimensions(shape), values, 0n) == Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)) : Nat}:
133 Equal.trans(Nat, Shape.horner(Shape.dimensions(shape), values, 0n), Shape.offset(Shape.extents(shape), Shape.naturals(values)), Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)), Coordinates.horner_spec(Shape.dimensions(shape), values, 0n, fits), Equal.sym(Nat, Shape.row_major(Shape.extents(shape), Coordinates.coordinate_of(Shape.extents(shape), Shape.naturals(values), fits)), Shape.offset(Shape.extents(shape), Shape.naturals(values)), Coordinates.offset_of(Shape.extents(shape), Shape.naturals(values), fits)))