summaryrefslogtreecommitdiff
path: root/src/Helium/Data
diff options
context:
space:
mode:
Diffstat (limited to 'src/Helium/Data')
-rw-r--r--src/Helium/Data/Pseudocode/Types.agda2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Types.agda
index 971ca12..dbd3c6b 100644
--- a/src/Helium/Data/Pseudocode/Types.agda
+++ b/src/Helium/Data/Pseudocode/Types.agda
@@ -146,3 +146,5 @@ record Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃ :
; _/1 = _/1
; ⌊_⌋ = ⌊_⌋
}
+
+ open RawPseudocode rawPseudocode using (module ℤ′; module ℝ′) public