Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Merge pull request #1 from glguy/master

Be explicit about uninferable types
  • Loading branch information...
commit e57e4b279f3b0536113d45348448366f9317e576 2 parents a368319 + 6550528
@copumpkin authored
Showing with 3 additions and 3 deletions.
  1. +3 −3 Data/BitVector/Properties.agda
View
6 Data/BitVector/Properties.agda
@@ -306,10 +306,10 @@ private
| *-comm x y
| *-comm x z = refl
- module Properties n where
+ module Properties (n : ℕ) where
open import Algebra.Structures
- +-isSemigroup : IsSemigroup _≡_ _+_
+ +-isSemigroup : IsSemigroup {A = BitVector n} _≡_ _+_
+-isSemigroup = record
{ isEquivalence = isEquivalence; assoc = +-assoc; ∙-cong = cong₂ _+_ }
@@ -324,7 +324,7 @@ private
+-isAbelianGroup : IsAbelianGroup _≡_ _+_ (zero n) -_
+-isAbelianGroup = record { isGroup = +-isGroup; comm = +-comm }
- *-isSemigroup : IsSemigroup _≡_ _*_
+ *-isSemigroup : IsSemigroup {A = BitVector n} _≡_ _*_
*-isSemigroup = record
{ isEquivalence = isEquivalence; assoc = *-assoc; ∙-cong = cong₂ _*_ }
Please sign in to comment.
Something went wrong with that request. Please try again.