~/jendhub

def fin_of_value

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

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/LAWS.bend as Laws

30def fin_of_value(+bound: Nat, +index: Shape.Fin(bound)) -> {Some{index} == Laws.fin_of(bound, Shape.Fin.value(bound, index)) : Maybe<&2, Shape.Fin(bound)>}:
31  match bound:
32    case 0n:
33      match index:
34    case 1n+p:
35      match index:
36        case Shape.FZero{}:
37          {==}
38        case Shape.FNext{+previous}:
39          Equal.cong(Maybe<&2, Shape.Fin(p)>, Maybe<&2, Shape.Fin(1n+p)>, index => Laws.fin_of.next(p, index), Some{previous}, Laws.fin_of(p, Shape.Fin.value(p, previous)), fin_of_value(p, previous))

Uses (8)

Used by (1)