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 gmail.com> 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"
> Thanks in advance.
This archive was generated by a fusion of
Pipermail (Mailman edition) and