In general, how do I use typedef constructors in code?
As a more specific example, how do I use Dlist?
I have this code & encounter these errors:
theory test imports Main "~~/src/HOL/Library/Dlist" begin (* No code equations for Dlist.abs_dlist *) value "Dlist.abs_dlist [1,2,1] :: nat dlist" (* Abstraction violation: constant Dlist *) value "Dlist.Dlist [1,2,1] :: nat dlist"
I thought that
setup_lifting type_definition_dlist would produce the necessary code?
I also thought that this would generate code:
lemma Dlist_list_of_dlist [simp, code abstype]: "Dlist (list_of_dlist dxs) = dxs" by (simp add: Dlist_def list_of_dlist_inverse distinct_remdups_id)
Last updated: Aug 15 2022 at 02:13 UTC