Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int
On 2/8/2014 2:13 PM, Gottfried Barrow wrote:
class lord_fieldNN_2 = field +
fixes NNeg :: "'a set"
assumes plusClosed: "x + y : NNeg"
assumes timesClosed: "x * y : NNeg"
assumes trichotomy: "x = 0 | x : NNeg | -x : NNeg" (*Needs an
No one cares I'm sure, but, for closure, I didn't put in the condition
that the elements be in NNeg, where I guess I should have used P instead
This archive was generated by a fusion of
Pipermail (Mailman edition) and