ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-11 14:57:30 +03:00
Code Issues Projects Releases Wiki Activity

Comment out VerifiedField and subclasses for now

Browse Source
This commit is contained in:
Cliff Harvey 2015-04-11 22:55:58 +02:00
parent be22ac6307
commit cc86ef0bbe
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
libs/contrib/Classes/Verified.idr
View File

@ -80,9 +80,9 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
total ringWithUnityIsUnityL : (l : a) -> l <.> unity = l
total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
class (VerifiedRingWithUnity a, Field a) => VerifiedField a where
total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where
-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
class JoinSemilattice a => VerifiedJoinSemilattice a where
@ -108,10 +108,10 @@ class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice
class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }
class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v
total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where
-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v
-- total moduleScalarUnityIsUnity : (v : b) -> unity {a} <#> v = v
-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)
-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)
class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}
--class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}