summaryrefslogtreecommitdiff
path: root/src/Helium/Data
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2022-02-18 10:45:35 +0000
committerGreg Brown <greg.brown@cl.cam.ac.uk>2022-02-18 10:45:35 +0000
commitad5322977632dd2dcec7cb75082d5c128b4a8bd5 (patch)
tree82844d4d25a6017713ed0da0a54f4a16d55f8fe9 /src/Helium/Data
parent60b201d0c8752b84194753bb72eee777bf245fe3 (diff)
Remove declare case of Procedure.
Diffstat (limited to 'src/Helium/Data')
-rw-r--r--src/Helium/Data/Pseudocode/Core.agda1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/Helium/Data/Pseudocode/Core.agda b/src/Helium/Data/Pseudocode/Core.agda
index 4728e44..4dbf552 100644
--- a/src/Helium/Data/Pseudocode/Core.agda
+++ b/src/Helium/Data/Pseudocode/Core.agda
@@ -253,7 +253,6 @@ module Code {o} (Σ : Vec Type o) where
data Procedure Γ where
_∙end : Statement Γ → Procedure Γ
- declare : ∀ {t} → Expression Γ t → Procedure (t ∷ Γ) → Procedure Γ
infixl 6 _<<_
infixl 5 _-_