Function arr_ext_persistent_array_ty 

pub fn arr_ext_persistent_array_ty() -> Expr

PersistentArray : Type → Nat → Type

A persistent (purely functional) array: all versions of the array are accessible after updates. Implemented via balanced binary trees or path copying, supporting O(log n) access and update.