git.iko.soy/Idris-dev
on master help sign in
Add access clause.
7761b7aSventimir
libs/contrib/Control/Algebra/Laws.idr+1
compare with master
unifiedsplit
@@ -4,6 +4,7 @@ import Prelude.Algebra as A
4import Control.Algebra
4import Control.Algebra
5import Interfaces.Verified
5import Interfaces.Verified
6
6
7+%access export
7
8
8inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
9inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
9inverseNeutralIsNeutral {t} =
10inverseNeutralIsNeutral {t} =