Add some convenience functions.

1 files changed, 8 insertions, 0 deletions

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