gistfile1.txt

module Test

import Algebra.AbstractAlgebra

data Test : Type where
    test : Test

instance Semigroup Test where
    test <+> test = test

instance Monoid Test where
    neutral = test

instance Group Test where
    inverse test = test

instance AbelianGroup Test where {}

instance Ring Test where
   test <*> test = test

instance RingWithUnity Test where
   unity = test

instance Field Test where
   inverseM test = test

-- Consider the case of a Field 'Test' as a VectorSpace over itself
instance VectorSpace Test Test where {}




instance VerifiedSemigroup Test where
    semigroupOpIsAssociative test test test = Refl

instance VerifiedMonoid Test where
    monoidNeutralIsNeutralL test = Refl
    monoidNeutralIsNeutralR test = Refl

instance VerifiedGroup Test where
    groupInverseIsInverseL test = Refl
    groupInverseIsInverseR test = Refl

instance VerifiedAbelianGroup Test where
    abelianGroupOpIsCommutative test test = Refl

instance VerifiedRing Test where
    ringOpIsAssociative   test test test = Refl
    ringOpIsDistributiveL test test test = Refl
    ringOpIsDistributiveR test test test = Refl

instance VerifiedRingWithUnity Test where
    ringWithUnityIsUnityL test = Refl
    ringWithUnityIsUnityR test = Refl

instance VerifiedField Test where
    fieldInverseIsInverseL test = Refl
    fieldInverseIsInverseR test = Refl