From 0b581ec922b40284291d6814578bd2e68049c8b7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 21 Dec 2021 15:14:54 +0000
Subject: Define execBeats, a wrapper to execute beat-wise instructions.

---
 src/Helium/Data/Pseudocode.agda | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'src/Helium/Data')

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 3f82cf0..9982501 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -23,7 +23,7 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
   infix 8 _⁻¹
   infixr 7 _*ᶻ_ _*ʳ_
   infix 6 -ᶻ_ -ʳ_
-  infixr 5 _+ᶻ_ _+ʳ_
+  infixr 5 _+ᶻ_ _+ʳ_ _∶_
   infix 4 _≈ᵇ_ _≟ᵇ_ _≈ᶻ_ _≟ᶻ_ _<ᶻ_ _<?ᶻ_ _≈ʳ_ _≟ʳ_ _<ʳ_ _<?ʳ_
 
   field
@@ -83,6 +83,10 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
   zeros {zero}  = []
   zeros {suc n} = 0b ∶ zeros
 
+  ones : ∀ {n} → Bits n
+  ones {zero}  = []
+  ones {suc n} = 1b ∶ ones
+
   _eor_ : ∀ {n} → Op₂ (Bits n)
   x eor y = (x or y) and not (x and y)
 
-- 
cgit v1.2.3