Re: [isabelle] Reasoning about types

On Thu, 22 Dec 2011, John Munroe wrote:

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

No, types are somewhat restrained. The HOL community has accumulated certain smart tricks to do funny things with the little flexibilty that the type language provides, see src/HOL/Library/Numeral_Type.thy for example.


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