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 exclusive or.*)

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 of NNeg.





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