From 880afa3416b51bfdc49973adee41f1b31bf80f47 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Wed, 13 Apr 2022 15:58:15 -0500 Subject: [PATCH] Unbitrotting --- prototyping/Properties/Subtyping.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index e4fc3799..48eff0dc 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -142,10 +142,10 @@ function-ok-tgt unknown = unknown tgt-¬function-ok : ∀ {T t} → (¬Language (tgt T) t) → ¬Language T (function-ok t) tgt-¬function-ok {T = nil} p = scalar-function-ok nil tgt-¬function-ok {T = T₁ ⇒ T₂} p = function-ok p -tgt-¬function-ok {T = none} p = none -tgt-¬function-ok {T = any} (scalar-scalar s () p) -tgt-¬function-ok {T = any} (scalar-function ()) -tgt-¬function-ok {T = any} (scalar-function-ok ()) +tgt-¬function-ok {T = never} p = never +tgt-¬function-ok {T = unknown} (scalar-scalar s () p) +tgt-¬function-ok {T = unknown} (scalar-function ()) +tgt-¬function-ok {T = unknown} (scalar-function-ok ()) tgt-¬function-ok {T = boolean} p = scalar-function-ok boolean tgt-¬function-ok {T = number} p = scalar-function-ok number tgt-¬function-ok {T = string} p = scalar-function-ok string