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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.