[isabelle-dev] sets and code generation

[Lukas Bulwahn]

On 03/23/2012 11:45 AM, Jesus Aransay wrote:
> I know there is an alternative way to get that, by means of sparse
> matrices (SparseMatrix.thy), but it demands translating every
> operation over the matrix type to its equivalent version for "sparse
> matrices", which may be sometimes hard work.
>
Code generation often requires translating or transfering every 
operation from one type to another. At the moment, users have to do this 
manually (which can be hard work as you said), but we are working on a 
mechanism that should soon automate this.


Lukas