[isabelle-dev] sets and code generation

Lukas Bulwahn bulwahn at in.tum.de
Fri Mar 23 12:31:10 CET 2012

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.


More information about the isabelle-dev mailing list