diff options
| author | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 17:43:43 +0000 |
|---|---|---|
| committer | Greg Brown <greg.brown@cl.cam.ac.uk> | 2021-12-20 17:43:43 +0000 |
| commit | e32ce3737798d4519c5497c36e912e92d60bd36b (patch) | |
| tree | b737199dbc1d8ccadfc775be6cb1d966474b5035 /src/Helium/Semantics/Denotational | |
| parent | ee7e46719f428c61ef785ec791c341ddb350cc40 (diff) | |
Define semantics of vhsub.
Diffstat (limited to 'src/Helium/Semantics/Denotational')
| -rw-r--r-- | src/Helium/Semantics/Denotational/Core.agda | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Helium/Semantics/Denotational/Core.agda b/src/Helium/Semantics/Denotational/Core.agda index a0a37e8..bf5f20f 100644 --- a/src/Helium/Semantics/Denotational/Core.agda +++ b/src/Helium/Semantics/Denotational/Core.agda @@ -75,8 +75,8 @@ _<*>_ f e σ ρ = f σ ρ >>= λ (σ , f) → apply f e σ ρ !_ : ∀ {n ls} {Γ : Sets n ls} → Reference n Γ τ → Expr n Γ τ ! r = Reference.get r -call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product⊤ m Γ) → Expr n Δ τ -call f e σ ρ = e σ ρ >>= λ (σ , v) → f unknown σ v +call : ∀ {m n ls₁ ls₂} {Γ : Sets m ls₁} {Δ : Sets n ls₂} → Function m Γ τ → Expr n Δ (Product m Γ) → Expr n Δ τ +call f e σ ρ = e σ ρ >>= λ (σ , v) → f unknown σ (toProduct⊤ _ v) -- References |