Add access clause.
commit7761b7a1b61c4e352c938df65c345d8ffa12cdcc
authorSventimir <svantimir@gmail.com>
dateSat 16 Mar 2019, 11:42 (8 years ago)
parentbcce759
libs/contrib/Control/Algebra/Laws.idr+1
@@ -4,6 +4,7 @@ import Prelude.Algebra as A
44import Control.Algebra
55import Interfaces.Verified
66
7+%access export
78
89inverseNeutralIsNeutral : VerifiedGroup t => inverse (the t A.neutral) = A.neutral
910inverseNeutralIsNeutral {t} =