Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes



Hi Jasmin,

> The low-level theorems you'd need, e.g. "ctor_dtor", are stored in the BNF (co)datatype database:
> 
>     ML {*
>     BNF_FP_Def_Sugar.fp_sugar_of @{context} @{type_name bintree}
>     |> the
>     |> #fp_res
>     |> #ctor_dtors
>     |> hd
>     *}

this is very nifty, thanks for the hint! Maybe at some point we can use
this to support generic programming à la de Vries & LÃh
(<http://www.andres-loeh.de/TrueSumsOfProducts/TrueSumsOfProducts.pdf>).

Cheers
Lars





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