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

WIP

Browse source
This commit is contained in:
ajeffrey@roblox.com 2022-05-25 16:02:27 -05:00
parent 3b55f94066
commit d17804768e
1 changed files with 5 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
prototyping/Properties/Subtyping.agda
View file

@ -285,16 +285,15 @@ language-comp (function-tgt t) (function-tgt p) (function-tgt q) = language-comp
<:-function-left p s Rs | Left ¬Ss with p (function-err s) (function-err ¬Ss)
<:-function-left p s Rs | Left ¬Ss | function-err ¬Rs = CONTRADICTION (language-comp s ¬Rs Rs)
<:-function-right : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (R ≮: never) → (T <: U)
<:-function-right p (witness s Rs never) t Tt with p (function-ok s t) (function-ok₂ Tt)
<:-function-right p (witness s Rs never) t Tt | function-ok₁ ¬Rs = CONTRADICTION (language-comp s ¬Rs Rs)
<:-function-right p (witness s Rs never) t Tt | function-ok₂ St = St
<:-function-right : ∀ {R S T U} → (S ⇒ T) <: (R ⇒ U) → (T <: U)
<:-function-right p t Tt with p (function-tgt t) (function-tgt Tt)
<:-function-right p t Tt | function-tgt St = St
≮:-function-left : ∀ {R S T U} → (R ≮: S) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-left (witness t p q) = witness (function-err t) (function-err q) (function-err p)
≮:-function-right : ∀ {R S T U} → (R ≮: never) → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-right (witness s r _) (witness t p q) = witness (function-ok s t) (function-ok₂ p) (function-ok r q)
≮:-function-right : ∀ {R S T U} → (T ≮: U) → (S ⇒ T) ≮: (R ⇒ U)
≮:-function-right (witness t p q) = witness (function-tgt t) (function-tgt p) (function-tgt q)
-- Properties of scalars
skalar-function-ok : ∀ {s t} → (¬Language skalar (function-ok s t))