From 165d3912c9fbcd217b0f2044cce28ad5b0f2d563 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 5 Jul 2024 16:47:26 +1000 Subject: [PATCH] [squash] address FIXMEs after PR comments/discussion --- docs/arch-split.md | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/docs/arch-split.md b/docs/arch-split.md index c488684162..39705dd083 100644 --- a/docs/arch-split.md +++ b/docs/arch-split.md @@ -296,7 +296,6 @@ multiple facts). This disparity will only get worse as the Arch context grows bigger, and might indicate the need for some alternative functionality. -(FIXME: check if this is true) ### Dealing with name clashes @@ -643,10 +642,12 @@ interpretation Foo_AI_2?: Foo_AI_2 (* now we get access to GD in the global context *) ``` -FIXME: strictly speaking, there is no requirement that `Foo_AI_2` includes -`Foo_AI_1`, but in practice we always do so (I guess because we want everything -that got proved to be instantly available in case we need it in the proof -chain). This would mean that the same fact gets exported multiple times? +While strictly speaking, there is no requirement that `Foo_AI_2` includes +`Foo_AI_1`, in practice we always do so, since we want everything that got +proved to be instantly available in case it's needed in the proof chain. This +generates limited duplication: a fact from `Foo_AI_1` will be duplicated in +`Foo_AI_2`, but not in `Foo_AI_3+`. + ## Qualifying non-locale-compatible commands