From 7499f040c1dcaeb645d97fe59076ccf59128162a Mon Sep 17 00:00:00 2001 From: "ajeffrey@roblox.com" Date: Fri, 22 Apr 2022 19:56:38 -0500 Subject: [PATCH] WIP --- prototyping/Properties/TypeNormalization.agda | 18 +++--------------- 1 file changed, 3 insertions(+), 15 deletions(-) diff --git a/prototyping/Properties/TypeNormalization.agda b/prototyping/Properties/TypeNormalization.agda index 47584c17..c5f4546c 100644 --- a/prototyping/Properties/TypeNormalization.agda +++ b/prototyping/Properties/TypeNormalization.agda @@ -51,31 +51,19 @@ normal (S ∩ T) = normal-∩ⁿ (normal S) (normal T) normalᶠ (S ⇒ T) = S ⇒ T normalᶠ (F ∩ G) = F ∩ G -normal-∪ⁿ never never = never -normal-∪ⁿ never unknown = unknown +normal-∪ⁿ S (T₁ ∪ T₂) = (normal-∪ⁿ S T₁) ∪ T₂ +normal-∪ⁿ S never = S +normal-∪ⁿ S unknown = unknown normal-∪ⁿ never (T ⇒ U) = T ⇒ U normal-∪ⁿ never (G₁ ∩ G₂) = G₁ ∩ G₂ -normal-∪ⁿ never (T₁ ∪ T₂) = (normal-∪ⁿ never) T₁ ∪ T₂ -normal-∪ⁿ unknown never = unknown -normal-∪ⁿ unknown unknown = unknown normal-∪ⁿ unknown (T ⇒ U) = unknown normal-∪ⁿ unknown (G₁ ∩ G₂) = unknown -normal-∪ⁿ unknown (T₁ ∪ T₂) = (normal-∪ⁿ unknown T₁) ∪ T₂ -normal-∪ⁿ (R ⇒ S) never = (R ⇒ S) -normal-∪ⁿ (R ⇒ S) unknown = unknown normal-∪ⁿ (R ⇒ S) (T ⇒ U) = normalᶠ (normal-∪ᶠ (R ⇒ S) (T ⇒ U)) normal-∪ⁿ (R ⇒ S) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (R ⇒ S) (G₁ ∩ G₂)) -normal-∪ⁿ (R ⇒ S) (T₁ ∪ T₂) = (normal-∪ⁿ (R ⇒ S) T₁) ∪ T₂ -normal-∪ⁿ (F₁ ∩ F₂) never = (F₁ ∩ F₂) -normal-∪ⁿ (F₁ ∩ F₂) unknown = unknown normal-∪ⁿ (F₁ ∩ F₂) (T ⇒ U) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (T ⇒ U)) normal-∪ⁿ (F₁ ∩ F₂) (G₁ ∩ G₂) = normalᶠ (normal-∪ᶠ (F₁ ∩ F₂) (G₁ ∩ G₂)) -normal-∪ⁿ (F₁ ∩ F₂) (T₁ ∪ T₂) = (normal-∪ⁿ (F₁ ∩ F₂) T₁) ∪ T₂ -normal-∪ⁿ (S₁ ∪ S₂) never = S₁ ∪ S₂ -normal-∪ⁿ (S₁ ∪ S₂) unknown = unknown normal-∪ⁿ (S₁ ∪ S₂) (T₁ ⇒ T₂) = normal-∪ⁿ S₁ (T₁ ⇒ T₂) ∪ S₂ normal-∪ⁿ (S₁ ∪ S₂) (G₁ ∩ G₂) = normal-∪ⁿ S₁ (G₁ ∩ G₂) ∪ S₂ -normal-∪ⁿ (S₁ ∪ S₂) (T₁ ∪ T₂) = normal-∪ⁿ (S₁ ∪ S₂) T₁ ∪ T₂ -- normal-∪ⁿ never never = never -- normal-∪ⁿ never unknown = unknown