From 855f823999e1090386e538b7ec02a286e55131e7 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 20 Dec 2021 14:31:30 +0000
Subject: Add some convenience functions.

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

(limited to 'src/Helium')

diff --git a/src/Helium/Data/Pseudocode.agda b/src/Helium/Data/Pseudocode.agda
index 2a31055..61a6b23 100644
--- a/src/Helium/Data/Pseudocode.agda
+++ b/src/Helium/Data/Pseudocode.agda
@@ -136,6 +136,8 @@ 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
 
@@ -165,3 +167,9 @@ record RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ : Set (ℓsuc (b₁
     eq : ∀ {n} (i : Fin n) → toℕ (suc i - inject₁ (strengthen i)) ≡ 1
     eq zero    = refl
     eq (suc i) = eq i
+
+  -- Conveniences
+
+  zeros : ∀ {n} → Bits n
+  zeros {zero}  = []
+  zeros {suc n} = 0b ∶ zeros
-- 
cgit v1.2.3