Email Gateway (Aug 19 2022 at 13:52): Email Gateway (Aug 19 2022 at 13:52):From: Walther Neuper <wneuper@ist.tugraz.at>
I want to re-use an elaborated "typedef" (with identifier "ttt")
definition ppp :: "'a ⇒ bool" where "ppp p = True"
typedef 'a ttt = "{p::'a. ppp p}" unfolding ppp_def by auto
in a recursive datatype
datatype 'a ddd = C0 'a | Cn "('a ddd) ttt"
and get the understandable error message
Non-admissible type expression
'a ddd ttt
"Test.ttt" is not a datatype - can't use it in nested recursion
What is the best way to re-use "ttt" in "ddd" ?
Walther
Email Gateway (Aug 19 2022 at 13:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Walther,
The old datatype package supports recursion only through datatypes created by the old
datatype package (or registered with rep_datatype). The new datatype package
(~~/src/HOL/BNF/BNF) supports recursion through arbitrary bounded natural functors (BNFs).
However, typedefs are in general not bounded natural function. If your typedef is a BNF,
you can register it with the bnf command. Examples for registration can be found in
~~/src/HOL/BNF/More_BNFs.
Best,
Andreas
Email Gateway (Aug 19 2022 at 13:52):From: Walther Neuper <wneuper@ist.tugraz.at>
On 03/27/2014 09:35 AM, Andreas Lochbihler wrote:
Hi Walther,
The old datatype package supports recursion only through datatypes
created by the old datatype package (or registered with rep_datatype).
The new datatype package (~~/src/HOL/BNF/BNF) supports recursion
through arbitrary bounded natural functors (BNFs). However, typedefs
are in general not bounded natural function. If your typedef is a BNF,
you can register it with the bnf command.
Thank you very much!
Since our typedef is not a BNF, we would need a workaround, which I'll
shortcut by a simpler way (just a list) now.
Examples for registration can be found in ~~/src/HOL/BNF/More_BNFs.
Best,
AndreasOn 27/03/14 09:02, Walther Neuper wrote:
I want to re-use an elaborated "typedef" (with identifier "ttt")
definition ppp :: "'a ⇒ bool" where "ppp p = True"
typedef 'a ttt = "{p::'a. ppp p}" unfolding ppp_def by autoin a recursive datatype
datatype 'a ddd = C0 'a | Cn "('a ddd) ttt"
and get the understandable error message
Non-admissible type expression
'a ddd ttt
"Test.ttt" is not a datatype - can't use it in nested recursionWhat is the best way to re-use "ttt" in "ddd" ?
Walther
Last updated: Nov 21 2024 at 12:39 UTC