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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and