BoundaryProofs.decode_rank: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 90-100 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=90&end_line=100

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws

def decode_rank(+dims: List<&2, U32>, +values: List<&2, U32>, mismatch: {False{} == Nat.is_eq(Shape.rank_dimensions(dims), Shape.rank_dimensions(values)) : Bool}) -> {None{} == Laws.decode(Shape.naturals(dims), Shape.naturals(values)) : Maybe<&2, Shape.Coordinate(Shape.naturals(dims))>}:
  match dims values:
    case Nil{} Nil{}:
      Empty.absurd({None{} == Laws.decode(Nil{}, Nil{}) : Maybe<&2, Shape.Coordinate(Nil{})>}, Nats.contradiction(Nat.is_eq(0n, 0n), {==}, mismatch))
    case +dh <> +dt +vh <> +vt:
      %decode_rank(dt, vt, mismatch) : {None{} == Laws.decode.step(U32.to_nat(dh), Shape.naturals(dt), _, Laws.fin_of(U32.to_nat(dh), U32.to_nat(vh))) : Maybe<&2, Shape.Coordinate(Shape.naturals(dh <> dt))>}
      {==}
    case Nil{} vh <> vt:
      {==}
    case dh <> dt Nil{}:
      {==}

Uses (14):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=decode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=decode.step
  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/core.bend&name=Coordinate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=naturals
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=contradiction