Function arr_ext_persistent_get_ty 

pub fn arr_ext_persistent_get_ty() -> Expr

PersistentArray.get : {α : Type} → {n : Nat} → PersistentArray α n → Fin n → α

Persistent array lookup: O(log n) access without mutation.