bend-ml-tensor-array

Releases (20)

• 0.1.19.0 indexed
• 0.1.18.0 unindexed
• 0.1.17.0 unindexed
• 0.1.16.0 unindexed
• 0.1.15.0 unindexed
• 0.1.14.0 unindexed
• 0.1.13.0 unindexed
• 0.1.12.0 unindexed
• 0.1.11.0 unindexed
• 0.1.10.0 unindexed
• 0.1.9.0 unindexed
• 0.1.8.0 unindexed
• 0.1.7.0 unindexed
• 0.1.6.0 unindexed
• 0.1.5.0 unindexed
• 0.1.4.0 unindexed
• 0.1.3.0 unindexed
• 0.1.2.0 unindexed
• 0.1.1.0 unindexed
• 0.1.0.0 unindexed

Definitions (321)

main.bend

• law size_setLAW: writing v at i keeps the array's size (any i: the index wraps around)
• law get_after_setLAW: what Array.set writes at i, Array.get reads at i (any i: both wrap it the same way)
• def ASet.ApartASet.Apart(T, a, n, j, z, k, w): the write's descent (index j, first branch z) and the read's descent (k, w), both started from the size n, take different branches at some node of a before either reaches a leaf.
• def ASet.SideASet.Side: what a pass over a subtree the write does not enter proves: Array.size(a) is (a, ASet.sz(a)), and the pair a read along (n, k, w) returns is (its first component, its second)
• def ASet.side_node
• def ASet.side
• def ASet.ReadsASet.Reads: what one pass over the tree a proves about a write along (n, j, v, z) and a read along (n, k, w): 1.
• def ASet.WLthe written low half ASet.WL and the written high half ASet.WH of a node of size n
• def ASet.WH
• def ASet.RLthe read's descent into the low half and into the high half of a node of size n
• def ASet.RH
• def ASet.no_leaf
• def ASet.reads_tthe write goes into the low half xs
• def ASet.reads_fthe write goes into the high half ys
• def ASet.BothASet.Both: the six facts of the first two laws and the four of the third, from one pass
• def ASet.both_t
• def ASet.both_f
• def ASet.both
• def ASet.close_other
• def ASet.top_other
• law get_other_setLAW: a write at i leaves alone the cell a read at k reaches, when the two descents part before a leaf (any i and k: both wrap them; h is what makes them different cells, see the top of the file)