summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2022-03-20 14:05:57 +0000
committerGreg Brown <greg.brown@cl.cam.ac.uk>2022-03-20 14:05:57 +0000
commit0ceb2b6f579c94fe82dbe17e073408145f637fcb (patch)
tree4c2444d6d13538af5369f51ef1b1e695b7a937a6 /src
parent2d204577f2e2f1a7e097971938561ad92b613d92 (diff)
Rename Pseudocode.Types to something more sensible
Diffstat (limited to 'src')
-rw-r--r--src/Helium/Data/Pseudocode/Algebra.agda (renamed from src/Helium/Data/Pseudocode/Types.agda)2
-rw-r--r--src/Helium/Semantics/Axiomatic/Assertion.agda2
-rw-r--r--src/Helium/Semantics/Axiomatic/Core.agda2
-rw-r--r--src/Helium/Semantics/Axiomatic/Term.agda2
-rw-r--r--src/Helium/Semantics/Axiomatic/Triple.agda2
-rw-r--r--src/Helium/Semantics/Denotational/Core.agda2
6 files changed, 6 insertions, 6 deletions
diff --git a/src/Helium/Data/Pseudocode/Types.agda b/src/Helium/Data/Pseudocode/Algebra.agda
index 6ea9cd2..523150d 100644
--- a/src/Helium/Data/Pseudocode/Types.agda
+++ b/src/Helium/Data/Pseudocode/Algebra.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --safe --without-K #-}
-module Helium.Data.Pseudocode.Types where
+module Helium.Data.Pseudocode.Algebra where
open import Algebra.Core
import Algebra.Definitions.RawSemiring as RS
diff --git a/src/Helium/Semantics/Axiomatic/Assertion.agda b/src/Helium/Semantics/Axiomatic/Assertion.agda
index 8192e5f..ab786e5 100644
--- a/src/Helium/Semantics/Axiomatic/Assertion.agda
+++ b/src/Helium/Semantics/Axiomatic/Assertion.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --safe --without-K #-}
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
module Helium.Semantics.Axiomatic.Assertion
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
index 3b7e8db..a65a6d0 100644
--- a/src/Helium/Semantics/Axiomatic/Core.agda
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --safe --without-K #-}
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
module Helium.Semantics.Axiomatic.Core
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
index 2719455..57dad92 100644
--- a/src/Helium/Semantics/Axiomatic/Term.agda
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --safe --without-K #-}
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
module Helium.Semantics.Axiomatic.Term
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Axiomatic/Triple.agda b/src/Helium/Semantics/Axiomatic/Triple.agda
index 7564983..23a487e 100644
--- a/src/Helium/Semantics/Axiomatic/Triple.agda
+++ b/src/Helium/Semantics/Axiomatic/Triple.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --safe --without-K #-}
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
module Helium.Semantics.Axiomatic.Triple
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda
index 0bd1794..090e0ba 100644
--- a/src/Helium/Semantics/Denotational/Core.agda
+++ b/src/Helium/Semantics/Denotational/Core.agda
@@ -6,7 +6,7 @@
{-# OPTIONS --safe --without-K #-}
-open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+open import Helium.Data.Pseudocode.Algebra using (RawPseudocode)
module Helium.Semantics.Denotational.Core
{b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}