def fin_of_from

bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:10

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
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws

10def fin_of_from(+bound: Nat, +value: Nat, fits: {True{} == Nat.is_lt(value, bound) : Bool}) -> {Laws.fin_of(bound, value) == Some{Coordinates.fin_from(bound, value, fits)} : Maybe<&2, Shape.Fin(bound)>}:
11  match bound value:
12    case 0n 0n:
13      Empty.absurd({Laws.fin_of(0n, 0n) == Some{Coordinates.fin_from(0n, 0n, fits)} : Maybe<&2, Shape.Fin(0n)>}, Shape.clash(fits))
14    case 0n 1n+q:
15      Empty.absurd({Laws.fin_of(0n, 1n+q) == Some{Coordinates.fin_from(0n, 1n+q, fits)} : Maybe<&2, Shape.Fin(0n)>}, Shape.clash(fits))
16    case 1n+p 0n:
17      {==}
18    case 1n+p 1n+q:
19      Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), Laws.fin_of(p, q), Some{Coordinates.fin_from(p, q, fits)}, fin_of_from(p, q, fits))