Email Gateway (Aug 22 2022 at 12:00): Email Gateway (Aug 22 2022 at 12:00):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I just noticed the following behaviour that I found a bit puzzling at first:
typedef 'a foo = "if finite (UNIV :: 'a :: finite set) then (UNIV :: 'a
set) else {}"
by auto
term "undefined :: nat foo"
Essentially, I define a type copy 'a foo for any finite type 'a;
however, Isabelle does not prevent me from using the type copy with an
infinite type like nat. I first thought that this must surely be
inconsistent, because I defined 'a foo to be empty for infinite types,
but to my relief, I found that all the lemmas generated by typedef are
annotated with the proper sort constraints, so it seems that "nat foo"
is logically /not/ an empty type, but more like a completely arbitrary
(non-empty) type that I know nothing about.
My question now is this: is it possible to make writing "nat foo" a type
error? Or, perhaps, is it possible to add the sort constraint 'a ::
finite to the context if 'a foo appears anywhere?
My use case is that I use Fraction_Field from HOL-Library, which demands
its type parameter to be an idom, but whenever I have lemmas using 'a
fraction, I have to annotate 'a :: idom manually, which is annoying.
Cheers,
Manuel
Email Gateway (Aug 22 2022 at 12:00):From: Makarius <makarius@sketis.net>
No. Sorts do not affect the well-formedness of type-expressions, only the
logical meaning.
Makarius
Last updated: Apr 25 2024 at 04:18 UTC