luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-05-04 10:33:46 +01:00
Code Issues Projects Releases Packages Wiki Activity

Unbitrotting

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-04-13 15:58:15 -05:00
parent e9ee0ffdc9
commit 880afa3416
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
prototyping/Properties/Subtyping.agda
View file

@ -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