Ext for Lambdas in python API

[philzook58]

Is there a reason why the second argument of the Ext function cannot be a lambda term?

x = Real("x")
Ext(Lambda([x],x),Lambda([x],2*x))

Throws an error because the second argument is not an ArrayRef

z3/src/api/python/z3/z3.py

Line 4812 in 0405a59

_z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays")

[NikolajBjorner]

not sure why the check is so strong. The extensionality expression is for some reason exposed but tends to be of internal use.
Here is some background:
Ext makes sense only for one-dimensional arrays. Internally we create indexed versions for multi-dimensional arrays but opted to only first expose one dimensional array sorts over API to keep it manageable. Thus, the version of Ext for multi-dimensional arrays is not exposed and not supported.
Ext is the Skolem function for the axiom:

forall a, b. a != b => exists ext . a[ext] != b[ext]

When you Skolemize this axiom, ext becomes a function that takes to arrays as arguments and produces an index where they are different (if they are not different the index is arbitrary). You can also think of it as a choice function.