Stream: Beginner Questions

Topic: Typdefs and code

view this post on Zulip Daniel K (Jun 06 2022 at 03:18):

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"

view this post on Zulip Daniel K (Jun 06 2022 at 03:19):

I thought that setup_lifting type_definition_dlist would produce the necessary code?

view this post on Zulip Daniel K (Jun 06 2022 at 03:19):

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: Dec 21 2024 at 16:20 UTC