LAWS.unflatten_checked_refines: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as LAWS
Lines 171-174 of bendtorch-core@0.1.0.0/src/shape/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&start_line=171&end_line=174

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

law unflatten_checked_refines:
  for +shape: Shape.Shape
  for +index: U32
  {coordinate_result(shape, Shape.unflatten_checked(shape, index)) == unflatten_spec(Shape.extents(shape), fin_of(Shape.numel(Shape.extents(shape)), U32.to_nat(index))) : Maybe<&2, List<&2, U32>>}

Uses (12):
  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=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=coordinate_result
  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=unflatten_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=unflatten_checked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten_checked