From d17804768e09714a8e34ce6be35a1063d79f6308 Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Wed, 25 May 2022 16:02:27 -0500 Subject: [PATCH] WIP --- prototyping/Properties/Subtyping.agda | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/prototyping/Properties/Subtyping.agda b/prototyping/Properties/Subtyping.agda index eb78b8db..44dd72e1 100644 --- a/prototyping/Properties/Subtyping.agda +++ b/prototyping/Properties/Subtyping.agda @@ -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))