def decode_none

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

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

41def decode_none(-dh: Nat, -dt: List<&2, Nat>, +tail: Maybe<&2, Shape.Coordinate(dt)>) -> {None{} == Laws.decode.step(dh, dt, tail, None{}) : Maybe<&2, Shape.Coordinate(dh <> dt)>}:
42  match tail:
43    case None{}:
44      {==}
45    case Some{rest}:
46      {==}