@@ -264,9 +264,42 @@ class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a w
264264
265265class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
266266
267+-- Fields.
268+||| Sets equipped with two binary operations, both associative and commutative
269+||| supplied with a neutral element, with
270+||| distributivity laws relating the two operations. Must satisfy the following
271+||| laws:
272+|||
273+||| + Associativity of `<+>`:
274+||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
275+||| + Commutativity of `<+>`:
276+||| forall a b, a <+> b == b <+> a
277+||| + Neutral for `<+>`:
278+||| forall a, a <+> neutral == a
279+||| forall a, neutral <+> a == a
280+||| + Inverse for `<+>`:
281+||| forall a, a <+> inverse a == neutral
282+||| forall a, inverse a <+> a == neutral
283+||| + Associativity of `<*>`:
284+||| forall a b c, a <*> (b <*> c) == (a <*> b) <*> c
285+||| + Unity for `<*>`:
286+||| forall a, a <*> unity == a
287+||| forall a, unity <*> a == a
288+||| + InverseM of `<*>`:
289+||| forall a, a <*> inverseM a == unity
290+||| forall a, inverseM a <*> a == unity
291+||| + Distributivity of `<*>` and `<->`:
292+||| forall a b c, a <*> (b <+> c) == (a <*> b) <+> (a <*> c)
293+||| forall a b c, (a <+> b) <*> c == (a <*> c) <+> (b <*> c)
294+class RingWithUnity a => Field a where
295+ inverseM : a -> a
296+
297+class (VerifiedRing a, Field a) => VerifiedField a where
298+ total fieldInverseIsInverseL : (l : a) -> l <*> inverseM l = unity
299+ total fieldInverseIsInverseR : (r : a) -> inverseM r <*> r = unity
267300
268301-- XXX todo:
269−-- Fields and vector spaces.
302+-- vector spaces.
270303-- Structures where "abs" make sense.
271304-- Euclidean domains, etc.
272305-- Where to put fromInteger and fromRational?