@@ -92,6 +92,11 @@ interface MeetSemilattice a => VerifiedMeetSemilattice a where
9292 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
9393 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
9494
95+{- FIXME: Some maintenance required here.
96+ Algebra.top and Algebra.bottom don't exist!
97+-}
98+{-
99+
95100interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
96101 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e
97102
@@ -112,3 +117,5 @@ interface (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, V
112117-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
113118
114119--interface (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
120+
121+-}