Re: [isabelle] Reasoning about types



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

Thanks

John

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