BoundaryProofs.fin_of_from: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 10-19 of bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&start_line=10&end_line=19

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

def 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)>}:
  match bound value:
    case 0n 0n:
      Empty.absurd({Laws.fin_of(0n, 0n) == Some{Coordinates.fin_from(0n, 0n, fits)} : Maybe<&2, Shape.Fin(0n)>}, Shape.clash(fits))
    case 0n 1n+q:
      Empty.absurd({Laws.fin_of(0n, 1n+q) == Some{Coordinates.fin_from(0n, 1n+q, fits)} : Maybe<&2, Shape.Fin(0n)>}, Shape.clash(fits))
    case 1n+p 0n:
      {==}
    case 1n+p 1n+q:
      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))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=fin_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=fin_of.next
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=clash