Re: [isabelle] typedef with sorts



On Tue, 8 Dec 2015, Manuel Eberl wrote:

My question now is this: is it possible to make writing "nat foo" a type error?

No. Sorts do not affect the well-formedness of type-expressions, only the logical meaning.


	Makarius




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