From 2ed2b3f6007ad497fc331c079ee2f74724b00669 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 8 Mar 2022 16:23:39 +0000
Subject: Add semantics of Hoare logic terms.

---
 src/Helium/Semantics/Axiomatic/Core.agda | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'src/Helium/Semantics/Axiomatic/Core.agda')

diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
index de4f411..3b7e8db 100644
--- a/src/Helium/Semantics/Axiomatic/Core.agda
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -60,6 +60,10 @@ private
 ⟦ [] ⟧ₜ′     = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤
 ⟦ t ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ ts ⟧ₜ′
 
+fetch : ∀ i → ⟦ Γ ⟧ₜ′ → ⟦ lookup Γ i ⟧ₜ
+fetch {Γ = _ ∷ _} 0F      (x , _)  = x
+fetch {Γ = _ ∷ _} (suc i) (_ , xs) = fetch i xs
+
 Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁)
 Transform ts t = ⟦ ts ⟧ₜ′ → ⟦ t ⟧ₜ
 
-- 
cgit v1.2.3