Library Stdlib.Array.PArray

From Stdlib Require Import Uint63.
From Stdlib Require Export PrimArray ArrayAxioms.

#[local] Open Scope uint63_scope.
#[local] Open Scope array_scope.





Lemma default_copy A (t:array A) : default (copy t) = default t.

Lemma default_make A (a : A) size : default (make size a) = a.

Lemma get_set_same_default A (t : array A) (i : int) :
  t.[i <- default t].[i] = default t.

Lemma get_not_default_lt A (t:array A) x :
 t.[x] <> default t -> (x <? length t) = true.