Stream: Beginner Questions

Topic: Is it possible to create a typedef of a typedef?


view this post on Zulip Hernán Rajchert (Mar 09 2023 at 04:26):

Hi, I'm trying to leverage fmap and create a new type with a restriction, but with this code

typedef Assets = "{assets. (∀ t v. fmlookup assets t = Some v ⟶ v > 0)} :: ((Token, nat) fmap) set"
proof
  show "fmempty ∈ {assets. (∀ t v. fmlookup assets t = Some v ⟶ v > 0)}"
    by auto
qed


setup_lifting type_definition_Assets

I have the following error on the last command

exception THM 1 raised (line 1872 of "thm.ML"):
  dest_state
  Quotient (fmrel (=)) (fmmap id) (fmmap id) (fmrel (=))

Is it possible to create a typedef of a typedef?

view this post on Zulip Wolfgang Jeltsch (Jun 04 2023 at 23:08):

I vaguely remember having had problems myself when trying something like this, and I cannot offer you a direct solution.

That said, it might make sense in your case to define the assets type differently. Spontaneously, I see the following two options:

By the way, the Isabelle convention is to have type names start with lower case letters.


Last updated: Feb 27 2024 at 08:17 UTC