Permalink
Browse files

Add fixity of _+_ and _*_

  • Loading branch information...
1 parent 887ab6b commit b89cd7c07dd5b0c9ad032af8248bda33b50340c7 @glguy glguy committed Sep 20, 2010
Showing with 3 additions and 3 deletions.
  1. +3 −3 Data/BitVector.agda
View
@@ -9,6 +9,9 @@ open import Data.Product
open import Data.Bool public hiding (_≟_) renaming (Bool to Bit; false to 0#; true to 1#)
+infixl 6 _+_
+infixl 7 _*_
+
BitVector = Vec Bit
bitwise-and : {n} Op₂ (BitVector n)
@@ -69,9 +72,6 @@ _*_ : ∀ {n} → Op₂ (BitVector n)
val10 = 0# ∷ 1# ∷ 0# ∷ 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []
val11 = 1# ∷ 1# ∷ 0# ∷ 1# ∷ 0# ∷ 0# ∷ 0# ∷ 0# ∷ []
--- Treat your BitVectors like peano naturals!
-
-
open import Relation.Nullary
open import Relation.Binary

0 comments on commit b89cd7c

Please sign in to comment.