Re: [isabelle] Reasoning about types

A related question: Are types first-class citizens in Isabelle/HOL?



On Thu, Dec 22, 2011 at 3:33 PM, John Munroe <munddr at> wrote:
> 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

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