BoundaryProofs.unflatten_verdict: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs Lines 165-177 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=165&end_line=177 import Base import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws def unflatten_verdict(+shape: Shape.Shape, +index: Nat, +verdict: Shape.BoolCase) -> {Laws.coordinate_result(shape, Shape.unflatten_checked.finish(shape, index, verdict)) == Laws.unflatten_spec(Shape.extents(shape), Laws.fin_of(Shape.numel(Shape.extents(shape)), index)) : Maybe<&2, List<&2, U32>>}: match verdict: case Shape.BFalse{equal}: %fin_of_none(Shape.numel(Shape.extents(shape)), index, Coordinates.size_misses(shape, index, equal)) : {None{} == Laws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>} {==} case Shape.BTrue{equal}: +fits = Coordinates.size_fits(shape, index, equal) +flat = Coordinates.fin_from(Shape.numel(Shape.extents(shape)), index, fits) %Equal.sym(Maybe<&2, Shape.Fin(Shape.numel(Shape.extents(shape)))>, Laws.fin_of(Shape.numel(Shape.extents(shape)), index), Some{flat}, fin_of_from(Shape.numel(Shape.extents(shape)), index, fits)) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.digits_words(Shape.dimensions(shape), index))) == Laws.unflatten_spec(Shape.extents(shape), _) : Maybe<&2, List<&2, U32>>} %Equal.sym(List<&2, Nat>, Shape.digits_words(Shape.dimensions(shape), index), Shape.digits(Shape.extents(shape), index), Coordinates.digits_words_spec(Shape.dimensions(shape), index)) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, _)) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>} %Coordinates.fin_from_value(Shape.numel(Shape.extents(shape)), index, fits) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, Shape.digits(Shape.extents(shape), _))) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>} %Coordinates.digits_unflatten(Shape.extents(shape), flat) : {Laws.coordinate_result(shape, Shape.coordinate_checked.nat(shape, _)) == Some{Shape.words(Shape.indices(Shape.extents(shape), Shape.unflatten(Shape.extents(shape), flat)))} : Maybe<&2, List<&2, U32>>} checked_indices(shape, Shape.unflatten(Shape.extents(shape), flat)) Uses (32): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym 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=Base/base.bend&name=U32 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=checked_indices https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fin_of_from 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/coordinate_proofs.bend&name=digits_unflatten https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=digits_words_spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from_value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=size_fits https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=size_misses 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=Fin 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=coordinate_checked.nat https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits_words https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements 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=indices 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 https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten_checked.finish https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=words