Re: [isabelle] Reasoning about types
On Thu, 22 Dec 2011, John Munroe wrote:
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"
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and