Email Gateway (Aug 18 2022 at 18:51): Email Gateway (Aug 18 2022 at 18:51):From: John Munroe <munddr@gmail.com>
Hi,
If a function f takes a type as an argument, is there a way to reason about
the 'parent' type of the argument type? Perhaps, something like:
Suppose U is a type.
definition "f s = (if s is a parent type of U then True else False"
Thanks in advance.
John
Email Gateway (Aug 18 2022 at 18:51):From: John Munroe <munddr@gmail.com>
A related question: Are types first-class citizens in Isabelle/HOL?
Thanks
John
Email Gateway (Aug 18 2022 at 18:52):From: Makarius <makarius@sketis.net>
It depends what exactly you mean by "is a parent type of". The Isabelle
framework allows some restricted reasoning about types, as cultivated
quite sucessfully for type classes, for example. Other (schematic)
relations over types also work, but there is no abstraction,
quantification, comparison of types.
Makarius
Email Gateway (Aug 18 2022 at 18:53):From: Makarius <makarius@sketis.net>
No, types are somewhat restrained. The HOL community has accumulated
certain smart tricks to do funny things with the little flexibilty that
the type language provides, see src/HOL/Library/Numeral_Type.thy for
example.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC