From 63f9978f448574d4df1ebacec52125a957482260 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 21 Dec 2021 13:41:20 +0000
Subject: Define semantics of vqdmulh.

---
 src/Helium/Data/Pseudocode.agda | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'src/Helium/Data')

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 5027784..3f82cf0 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -21,9 +21,9 @@ private
 record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ ⊔ b₂ ⊔ i₁ ⊔ i₂ ⊔ i₃ ⊔ r₁ ⊔ r₂ ⊔ r₃)) where
   infix 9 _^ᶻ_ _^ʳ_
   infix 8 _⁻¹
-  infix 7 _*ᶻ_ _*ʳ_
+  infixr 7 _*ᶻ_ _*ʳ_
   infix 6 -ᶻ_ -ʳ_
-  infix 5 _+ᶻ_ _+ʳ_
+  infixr 5 _+ᶻ_ _+ʳ_
   infix 4 _≈ᵇ_ _≟ᵇ_ _≈ᶻ_ _≟ᶻ_ _<ᶻ_ _<?ᶻ_ _≈ʳ_ _≟ʳ_ _<ʳ_ _<?ʳ_
 
   field
@@ -150,7 +150,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     (2^n≢0 : ∀ n → False (2ℤ ^ᶻ n ≟ᶻ 0ℤ))
     where
 
-    open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round
+    open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round public
 
     _>>_ : ℤ → ℕ → ℤ
     x >> n = (x div (2ℤ ^ᶻ n)) {2^n≢0 n}
@@ -167,8 +167,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x)
     where
 
-    open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round
-    open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0
+    open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 public
 
     sliceᶻ : ∀ n i → ℤ → Bits (n ℕ-ℕ i)
     sliceᶻ zero    zero    z = []
-- 
cgit v1.2.3