diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 18:58:23 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 18:58:23 +0000 |
| commit | 22b2a854fa02fd8c79a1351066922c0ba2e0cf42 (patch) | |
| tree | 97b925ae6c6a0fc98b322f70a42e1914faa9fdcb /src/Helium/Data | |
| parent | f81f771877b77ca1c6a6278d21153fa1c3df8d83 (diff) | |
Remove bitstring addition.
Diffstat (limited to 'src/Helium/Data')
| -rw-r--r-- | src/Helium/Data/Pseudocode.agda | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda index 6cf25ec..5027784 100644 --- a/src/Helium/Data/Pseudocode.agda +++ b/src/Helium/Data/Pseudocode.agda @@ -167,8 +167,6 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ (*ᶻ-identityʳ : ∀ x → x *ᶻ 1ℤ ≈ᶻ x) where - infix 5 _+ᵇ_ - open divmod ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round open 2^n≢0 ≈ᶻ-trans round∘⟦⟧ round-cong 0#-homo-round 2^n≢0 @@ -178,6 +176,3 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁ sliceᶻ (suc n) (suc i) z = sliceᶻ n i ((z div 2ℤ) {2≢0}) where 2≢0 = map-False (≈ᶻ-trans (*ᶻ-identityʳ 2ℤ)) (2^n≢0 1) - - _+ᵇ_ : ∀ {n} → Op₂ (Bits n) - x +ᵇ y = sliceᶻ _ zero (uint x +ᶻ uint y) |