proofs/containers/dynamic_array/owned_instances.bend checks
raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned_instances.bend as Owned_instances
4 imports
import Base import ../../../src/containers/dynamic_array.bend as A import ../../../src/containers/types/dynamic_array.bend as E import ./owned.bend as P
Definitions
def array_new_length source · line 7 · raw
{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(Array<U32>)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(Array<U32>), 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Nat)}Explicit checked instances: template declarations alone are not proof checks.
def array_new_capacity source · line 10 · raw
{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(Array<U32>)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(Array<U32>), 1n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Nat)}
def array_empty_pop source · line 13 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @a:Array<Maybe<&1, Array<U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, a}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.EmptyArray{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def array_swap_rejected source · line 16 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, Array<U32>>> -> @i:Nat -> @v:Array<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_checked_owned(Array<U32>, l, d, c, n, a, i, v, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<Array<U32>>, Maybe<&1, Array<U32>>>)}
def array_push_rejected source · line 19 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, Array<U32>>> -> @v:Array<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_room_owned(Array<U32>, l, d, c, n, a, v, False{}, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<Array<U32>>, Unit>)}
def array_update_rejected source · line 22 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, Array<U32>>> -> @i:Nat -> @f:(@_:Array<U32> -> Pair(Array<U32>, Array<U32>)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_checked_owned(Array<U32>, Array<U32>, l, d, c, n, a, i, f, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def array_first_push_pop source · line 25 · raw
@x:Array<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(Array<U32>, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<Array<U32>>, Unit>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(Array<U32>), x))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(Array<U32>), Done{x}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def array_first_swap source · line 28 · raw
@x:Array<U32> -> @y:Array<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, y) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{y}]}, Done{Some{x}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<Array<U32>>, Maybe<&1, Array<U32>>>)}
def array_first_update source · line 31 · raw
@x:Array<U32> -> @f:(@_:Array<U32> -> Pair(Array<U32>, Array<U32>)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_owned(Array<U32>, Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, f) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_put_owned(Array<U32>, Array<U32>, 31n, 0n, 1n, 1n, [None{}], 0n, f(x)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def array_clear_length source · line 34 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, Array<U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_owned(Array<U32>, d)}, 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Nat)}
def array_clear_capacity source · line 37 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, Array<U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_owned(Array<U32>, d)}, c) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, Array<U32>>, Nat)}
def array_first_drain source · line 40 · raw
@x:Array<U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.into_list_owned(Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}) == [x] : List<&1, Array<U32>>}
def nested_new_length source · line 43 · raw
{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>), 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Nat)}
def nested_new_capacity source · line 46 · raw
{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>), 1n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Nat)}
def nested_empty_pop source · line 49 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @a:Array<Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, a}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.EmptyArray{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>)}
def nested_swap_rejected source · line 52 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>> -> @i:Nat -> @v:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_checked_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, l, d, c, n, a, i, v, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>>)}
def nested_push_rejected source · line 55 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>> -> @v:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_room_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, l, d, c, n, a, v, False{}, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Unit>)}
def nested_update_rejected source · line 58 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>> -> @i:Nat -> @f:(@_:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Array<U32>)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_checked_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Array<U32>, l, d, c, n, a, i, f, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def nested_first_push_pop source · line 61 · raw
@x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Unit>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>), x))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>), Done{x}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>)}
def nested_first_swap source · line 64 · raw
@x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @y:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, y) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{y}]}, Done{Some{x}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>>)}
def nested_first_update source · line 67 · raw
@x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> @f:(@_:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Array<U32>)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, f) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_put_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, Array<U32>, 31n, 0n, 1n, 1n, [None{}], 0n, f(x)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def nested_clear_length source · line 70 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, d)}, 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Nat)}
def nested_clear_capacity source · line 73 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, d)}, c) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>, Nat)}
def nested_first_drain source · line 76 · raw
@x:0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.into_list_owned(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}) == [x] : List<&1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&2, U32>>}
def closure_new_length source · line 79 · raw
{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(@_:U32 -> U32)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(@_:U32 -> U32), 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Nat)}
def closure_new_capacity source · line 82 · raw
{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(@_:U32 -> U32)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(@_:U32 -> U32), 1n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Nat)}
def closure_empty_pop source · line 85 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @a:Array<Maybe<&1, @_:U32 -> U32>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, a}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.EmptyArray{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, @_:U32 -> U32>)}
def closure_swap_rejected source · line 88 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, @_:U32 -> U32>> -> @i:Nat -> @v:(@_:U32 -> U32) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_checked_owned(@_:U32 -> U32, l, d, c, n, a, i, v, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<@_:U32 -> U32>, Maybe<&1, @_:U32 -> U32>>)}
def closure_push_rejected source · line 91 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, @_:U32 -> U32>> -> @v:(@_:U32 -> U32) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_room_owned(@_:U32 -> U32, l, d, c, n, a, v, False{}, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.CapacityExceeded{}, v}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<@_:U32 -> U32>, Unit>)}
def closure_update_rejected source · line 94 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, @_:U32 -> U32>> -> @i:Nat -> @f:(@_:(@_:U32 -> U32) -> Pair(@_:U32 -> U32, Array<U32>)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_checked_owned(@_:U32 -> U32, Array<U32>, l, d, c, n, a, i, f, False{}) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a}, Fail{0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.IndexOutOfRange{}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def closure_first_push_pop source · line 97 · raw
@x:(@_:U32 -> U32) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(@_:U32 -> U32, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<@_:U32 -> U32>, Unit>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(@_:U32 -> U32), x))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(@_:U32 -> U32), Done{x}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, @_:U32 -> U32>)}
def closure_first_swap source · line 100 · raw
@x:(@_:U32 -> U32) -> @y:(@_:U32 -> U32) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, y) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{y}]}, Done{Some{x}}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<@_:U32 -> U32>, Maybe<&1, @_:U32 -> U32>>)}
def closure_first_update source · line 103 · raw
@x:(@_:U32 -> U32) -> @f:(@_:(@_:U32 -> U32) -> Pair(@_:U32 -> U32, Array<U32>)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_owned(@_:U32 -> U32, Array<U32>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, f) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_put_owned(@_:U32 -> U32, Array<U32>, 31n, 0n, 1n, 1n, [None{}], 0n, f(x)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, Array<U32>>)}
def closure_clear_length source · line 106 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, @_:U32 -> U32>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_owned(@_:U32 -> U32, d)}, 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Nat)}
def closure_clear_capacity source · line 109 · raw
@l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, @_:U32 -> U32>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, n, a})) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{l, d, c, 0n, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.empty_owned(@_:U32 -> U32, d)}, c) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, @_:U32 -> U32>, Nat)}
def closure_first_drain source · line 112 · raw
@x:(@_:U32 -> U32) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.into_list_owned(@_:U32 -> U32, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}) == [x] : List<&1, @_:U32 -> U32>}