proofs/containers/dynamic_array/owned.bend checks

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/containers/dynamic_array/owned.bend as Owned

import Base
import ../../../src/containers/dynamic_array.bend as A
import ../../../src/containers/types/dynamic_array.bend as E

Templates

@-T:Type -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(T)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(T), 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Nat)}

@-T:Type -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(T)) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(T), 1n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Nat)}

@-T:Type -> @l:Nat -> @d:Nat -> @c:Nat -> @a:Array<Maybe<&1, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(T, 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, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)}

@-T:Type -> @l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, T>> -> @i:Nat -> @v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_checked_owned(T, 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, T>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Maybe<&1, T>>)}

@-T:Type -> @l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, T>> -> @v:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_room_owned(T, 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, T>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Unit>)}

@-T:Type -> @-R:Type -> @l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, T>> -> @i:Nat -> @f:(@_:T -> Pair(T, R)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_checked_owned(T, R, 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, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, R>)}

@-T:Type -> @x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.pop_owned(T, Pair.fst(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Result<&1, &2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Unit>, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.push_owned(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(T), x))) == (0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.new_owned(T), Done{x}) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, T>)}

@-T:Type -> @x:T -> @y:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.swap_owned(T, 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, T>, Result<&1, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Rejected<T>, Maybe<&1, T>>)}

@-T:Type -> @-R:Type -> @x:T -> @f:(@_:T -> Pair(T, R)) -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_owned(T, R, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}, 0n, f) == 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.update_put_owned(T, R, 31n, 0n, 1n, 1n, [None{}], 0n, f(x)) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Result<&2, &1, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/types/dynamic_array.Error, R>)}

@-T:Type -> @l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.length_owned(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(T, 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(T, d)}, 0n) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Nat)}

@-T:Type -> @l:Nat -> @d:Nat -> @c:Nat -> @n:Nat -> @a:Array<Maybe<&1, T>> -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.capacity_owned(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.clear_owned(T, 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(T, d)}, c) : Pair(0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DynArray<&1, T>, Nat)}

@-T:Type -> @x:T -> {0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.into_list_owned(T, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/src/containers/dynamic_array.DA{31n, 0n, 1n, 1n, [Some{x}]}) == [x] : List<&1, T>}