diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-16 16:00:08 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2022-02-16 16:00:08 +0000 |
| commit | 273b6354ea17be93a0dfe4f50cd047b328762b02 (patch) | |
| tree | 580a926199dd89f84168d050f8db0a379f0171f8 /src/Helium/Data | |
| parent | 78aad93db3d7029e0a9a8517a2db92533fd1f401 (diff) | |
Begin work on axiomatic semantics.
Diffstat (limited to 'src/Helium/Data')
| -rw-r--r-- | src/Helium/Data/Pseudocode/Types.agda | 2 |
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 |