[isabelle-dev] sets and code generation
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