From 0f629700a4d8eee82e07d91b1165ac9df35eae42 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Thu, 21 Apr 2022 15:46:59 -0500 Subject: [PATCH] WIP --- prototyping/Properties/StrictMode.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/prototyping/Properties/StrictMode.agda b/prototyping/Properties/StrictMode.agda index 61fbec5c..30732cac 100644 --- a/prototyping/Properties/StrictMode.agda +++ b/prototyping/Properties/StrictMode.agda @@ -23,7 +23,7 @@ open import Properties.Dec using (Dec; yes; no) open import Properties.Contradiction using (CONTRADICTION; ¬) open import Properties.Functions using (_∘_) open import Properties.DecSubtyping using (dec-subtyping) -open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; never-tgt-≮:; tgt-never-≮:; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never) +open import Properties.Subtyping using (unknown-≮:; ≡-trans-≮:; ≮:-trans-≡; src-unknown-≮:; unknown-src-≮:; ≮:-trans; ≮:-refl; scalar-≢-impl-≮:; function-≮:-scalar; scalar-≮:-function; function-≮:-never; unknown-≮:-scalar; scalar-≮:-never; unknown-≮:-never) open import Properties.TypeCheck using (typeOfᴼ; typeOfᴹᴼ; typeOfⱽ; typeOfᴱ; typeOfᴮ; typeCheckᴱ; typeCheckᴮ; typeCheckᴼ; typeCheckᴴ) open import Luau.OpSem using (_⟦_⟧_⟶_; _⊢_⟶*_⊣_; _⊢_⟶ᴮ_⊣_; _⊢_⟶ᴱ_⊣_; app₁; app₂; function; beta; return; block; done; local; subst; binOp₀; binOp₁; binOp₂; refl; step; +; -; *; /; <; >; ==; ~=; <=; >=; ··) open import Luau.RuntimeError using (BinOpError; RuntimeErrorᴱ; RuntimeErrorᴮ; FunctionMismatch; BinOpMismatch₁; BinOpMismatch₂; UnboundVariable; SEGV; app₁; app₂; bin₁; bin₂; block; local; return; +; -; *; /; <; >; <=; >=; ··)