Function arr_ext_diff_array_ty 

pub fn arr_ext_diff_array_ty() -> Expr

Array.diff_array : {α : Type} → {n : Nat} → Array α n → Array α n

Difference array: for an array a, define d where d[0] = a[0], d[i] = a[i] - a[i-1]. Supports O(1) range update, O(n) reconstruction.