Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu



On 08/21/2016 07:35 PM, Ken Kubota wrote:
Dear Andrei,

Thank you for the quick answer, and also thanks to Larry Paulson and Makarius Wenzel.

I had read the abbreviated notation with the forall quantifier too quickly, but still the third restriction specified at
        http://sourceforge.net/projects/hol/files/hol/kananaskis-10/kananaskis-10-logic.pdf (p. 33) or at [Gordon/Melham, 1993, p. 220].
seems to be violated, as the type variable sigma occurs in the definiens, but not in (the type of) the definiendum.

That's a typo, that type should be tau, the type that was defined on the previous line. I've already uploaded an updated version of the draft.

Btw, we usually use alpha, beta, gamma for type variables, not sigma. But this is not mentioned until page 7.

Ondrej




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