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

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

def decode_unfit.step(+dh: Nat, +dt: List<&2, Nat>, +vh: Nat, +vt: List<&2, Nat>, +verdict: Shape.BoolCase<Nat.is_lt(vh, dh)>, misses: {False{} == Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)) : Bool}, rec: {False{} == Shape.fit(dt, vt) : Bool} -> {None{} == Laws.decode(dt, vt) : Maybe<&2, Shape.Coordinate(dt)>}) -> {None{} == Laws.decode.step(dh, dt, Laws.decode(dt, vt), Laws.fin_of(dh, vh)) : Maybe<&2, Shape.Coordinate(dh <> dt)>}:
  match verdict:
    case Shape.BFalse{equal}:
      %fin_of_none(dh, vh, equal) : {None{} == Laws.decode.step(dh, dt, Laws.decode(dt, vt), _) : Maybe<&2, Shape.Coordinate(dh <> dt)>}
      decode_none(dh, dt, Laws.decode(dt, vt))
    case Shape.BTrue{equal}:
      %rec(Equal.trans(Bool, False{}, Bool.and(Nat.is_lt(vh, dh), Shape.fit(dt, vt)), Shape.fit(dt, vt), misses, Equal.cong(Bool, Bool, head => Bool.and(head, Shape.fit(dt, vt)), Nat.is_lt(vh, dh), True{}, Equal.sym(Bool, True{}, Nat.is_lt(vh, dh), equal)))) : {None{} == Laws.decode.step(dh, dt, _, Laws.fin_of(dh, vh)) : Maybe<&2, Shape.Coordinate(dh <> dt)>}
      {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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
  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=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/boundary_proofs.bend&name=decode_none
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fin_of_none
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  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=fit