From 02f5e21331d98aeb4e356e103f3a30fb1fe6b9ae Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 24 Feb 2022 11:31:34 -0600 Subject: [PATCH] WIP --- prototyping/Examples/Run.agda | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/prototyping/Examples/Run.agda b/prototyping/Examples/Run.agda index 60f437f8..70863cc9 100644 --- a/prototyping/Examples/Run.agda +++ b/prototyping/Examples/Run.agda @@ -1,5 +1,4 @@ {-# OPTIONS --rewriting #-} -{-# OPTIONS --allow-unsolved-metas #-} module Examples.Run where @@ -9,10 +8,10 @@ open import Luau.Value using (nil; number) open import Luau.Run using (run; return) ex1 : (run (function "id" ⟨ var "x" ⟩ is return (var "x") ∙ done end ∙ return (var "id" $ nil) ∙ done) ≡ return nil _) -ex1 = {!!} +ex1 = refl ex2 : (run (function "fn" ⟨ var "x" ⟩ is return (number 123.0) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 123.0) _) -ex2 = {!!} +ex2 = refl ex3 : (run (function "fn" ⟨ var "x" ⟩ is return (binexp (number 1.0) + (number 2.0)) ∙ done end ∙ return (var "fn" $ nil) ∙ done) ≡ return (number 3.0) _) -ex3 = {!!} +ex3 = refl