From 781dbfa2b42f29ed727dd38c9f9e4f8dcaaf8f42 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Wed, 9 Feb 2022 15:32:59 -0600 Subject: [PATCH] Got examples to typecheck again --- prototyping/Examples/OpSem.agda | 2 +- prototyping/Examples/Run.agda | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/prototyping/Examples/OpSem.agda b/prototyping/Examples/OpSem.agda index a8d11080..4043869e 100644 --- a/prototyping/Examples/OpSem.agda +++ b/prototyping/Examples/OpSem.agda @@ -1,7 +1,7 @@ module Examples.OpSem where open import Luau.OpSem using (_⊢_⟶ᴱ_⊣_; _⊢_⟶ᴮ_⊣_; subst) -open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return; block_end) +open import Luau.Syntax using (var; nil; local_←_; _∙_; done; return) open import Luau.Heap using (emp) x = var "x" diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 573c1d06..bfa79839 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -14,5 +14,5 @@ import Agda.Builtin.Equality.Rewrite x = var "x" id = var "id" -ex1 : (run emp (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _) +ex1 : (run (function "id" ⟨ "x" ⟩ return x ∙ done end ∙ return (id $ nil) ∙ done) ≡ return nil _) ex1 = refl