[isabelle] Is it possible to get back at a list after encapsulating it in a plain function ( as in Gauss-Jordan-Elim-Fun ? )

       I am trying to encapsulate matrices/vectors/arrays/lists as functions, similar to the matrices in
Gauss-Jordan Elimination for Matrices Represented as Functions, but without passing the dimensions
For example,
definition "l2f (xs::'a list) = (λ (i::nat) . xs ! i)"
value "let a = l2f [10,11,12,13::real] in a 1"
Is it possible to define some
"( nat => 'a ) => nat" (the size of the original list)
"( nat => 'a ) => (nat × nat) " or "( nat => 'a ) => nat set" (the domain of the function) ?

If it is impossible to define a computable one, is it possible to define an incomputable specifictaion?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.