Definition foo local should prevent it from being _imported_. That works.
However, as soon as the containing module
bar is required,
bar.foo should IMHO work. That doesn't always work.
inside a file,
Local Definition works as I'd expect:
Module Import A. Local Definition test1 := 1. Definition test2 := 1. End A. Local Definition test2 := A.test1. Definition test3 := A.test1.
I'm more confused by the semantics wrt
Require Import D.testLocalDefA. (* OK *) Definition test3' := test3. Definition test3'a := testLocalDefA.test3. (* OK *) Fail Definition test3 := test2. Definition test3 := testLocalDefA.test2. (* WAT? *) Fail Definition test4 := A.test1. Definition test4 := testLocalDefA.A.test1. Definition test5 := A.test2. Definition test5' := testLocalDefA.A.test2.
A.test1 requires one more qualification than I'd expect. I have no idea why.
Import skips local definitions recursively?
Import A skips making
test1 available, correctly, but when
Import D.testLocalDefA imports
testLocalDefA, and it makes
A globally available, it recursively filters out
Local makes it so the only way to use a name is to qualify it completely.
"qualify it completely" is not true
I can skip the initial prefix
D for some reason, and however many levels appear there.
D.testLocalDefA. where instead
A.B.C.D.testLocalDefA., I'd just need to repeat
local instead? dunno)
(this assumes that
Import works by deep-copying dictionaries, instead of linking them, which is a pretty weird idea, but you can ignore that part if it doesn't help)
@Li-yao but would that semantics be useful/desirable/predictable?
things work as I'd expect without nested modules... so I noticed because I failed to make sense of the behavior
Okay I thought it was a little stricter than that. :shrug:
Well you weren't alone:
They [Definition and Example] can take the local attribute, which makes the defined ident accessible by Import and its variants only through their fully qualified names.
Modulo the prefix
D, your examples seem to work as described by that sentence, don't they?
Sorta. In another example, after
From bedrock.lang.cpp.logic Require Import simple_pointers., I can just start from
that is, if
Module A with local def
test1, you must write
so, my theory works if
simple_pointers is bound into the top-level by
Require (which ignores the
Local attribute), while
A is bound by
Import (which discards definitions marked
Probably worth an issue, to decide whether the documentation should be fixed or the behavior changed.
Local Definition means Import does nothing, but Require still has an effect
Require Foo makes Foo available without needing to prefix it
so for instance after
Require List. you can do
Import List. instead of having to do
Last updated: Feb 04 2023 at 22:29 UTC