From dd0a859aee9c4f1d1d8dbcb3bc764915dfc6d278 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Mon, 1 Sep 2025 17:01:04 +0200 Subject: [PATCH 1/2] Removing a requirement in `toi_promote` which is confusing and unnecessary --- resources/type-system/flow-analysis.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/resources/type-system/flow-analysis.md b/resources/type-system/flow-analysis.md index 2887dd9aba..4c72871a74 100644 --- a/resources/type-system/flow-analysis.md +++ b/resources/type-system/flow-analysis.md @@ -471,8 +471,8 @@ Definitions: _The types in `p1` are known as the types of interest._ - Let `p2` be the set `p1 \ { provisionalType }` _(where `\` denotes set difference)_. - - If the `written` type is in `p2`, and `written <: provisionalType`, then - `newPromotionChain` is `[...promotionChain, written]`. _Writing a value + - If the `written` type is in `p2` then `newPromotionChain` is + `[...promotionChain, written]`. _Writing a value whose static type is a type of interest promotes to that type._ - _By precondition, `written <: declared` and `written <: T` for all types in `promotionChain`. Therefore, `newPromotionChain` satisfies the From bd138e47bbc1b594f07d74147cc6fb6a3b179441 Mon Sep 17 00:00:00 2001 From: Erik Ernst Date: Mon, 1 Sep 2025 17:03:32 +0200 Subject: [PATCH 2/2] Whitespace --- resources/type-system/flow-analysis.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/resources/type-system/flow-analysis.md b/resources/type-system/flow-analysis.md index 4c72871a74..4fea666871 100644 --- a/resources/type-system/flow-analysis.md +++ b/resources/type-system/flow-analysis.md @@ -472,8 +472,8 @@ Definitions: - Let `p2` be the set `p1 \ { provisionalType }` _(where `\` denotes set difference)_. - If the `written` type is in `p2` then `newPromotionChain` is - `[...promotionChain, written]`. _Writing a value - whose static type is a type of interest promotes to that type._ + `[...promotionChain, written]`. _Writing a value whose static type is a + type of interest promotes to that type._ - _By precondition, `written <: declared` and `written <: T` for all types in `promotionChain`. Therefore, `newPromotionChain` satisfies the definition of a promotion chain, and is valid for declared type