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?
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:
0
as representing absence of a mapping. You should then define accessor functions that hide this implementation trick.By the way, the Isabelle convention is to have type names start with lower case letters.
Last updated: Nov 11 2024 at 01:24 UTC