diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-21 13:41:20 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-21 13:41:20 +0000 |
| commit | 63f9978f448574d4df1ebacec52125a957482260 (patch) | |
| tree | c9ad764891bf09074764fba02fa3c685468b0540 /src/Helium/Data/Pseudocode.agda | |
| parent | ef9f0202c1acae915f02ee2b39ab92981f800297 (diff) | |
Define semantics of vqdmulh.
Diffstat (limited to 'src/Helium/Data/Pseudocode.agda')
| -rw-r--r-- | src/Helium/Data/Pseudocode.agda | 9 |
1 files changed, 4 insertions, 5 deletions
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 = [] |