Stream: General

Topic: ✔ nested subtype, relator

view this post on Zulip Robert Soeldner (Sep 16 2021 at 11:11):

Consider the following example of a nested subtype:

typedef 'a A = "{a :: 'a fset . True}"
  by simp

setup_lifting type_definition_A

typedef 'a B = "{a :: 'a A. True}"
  by simp

setup_lifting type_definition_B

Here, the second setup_lifting of type B highlights, the missing relator of A.

Why does 'a A does not automatically have a relator?

From my understanding, a relator in this simple case would be

lift_definition rel_A :: "('a ⇒ 'b ⇒ bool) ⇒ 'a A  ⇒ 'b A ⇒ bool" is
"rel_fset" .

But what properties do I have to prove, to make it an "official" relator for the lifting package?

view this post on Zulip Robert Soeldner (Sep 18 2021 at 17:36):

The datatypes tutorial solved my issue. lift_bnf was the missing piece.

view this post on Zulip Notification Bot (Sep 18 2021 at 17:36):

Robert Soeldner has marked this topic as resolved.

Last updated: Apr 19 2024 at 20:15 UTC