49cff79712
This PR ensures private declarations are accessible from the private scope iff they are local or imported through an `import all` chain, including for anonymous notation and structure instance notation.
12 lines
207 B
Text
12 lines
207 B
Text
module
|
|
|
|
prelude
|
|
import all Module.ImportedAll
|
|
|
|
/-! `import all` should chain with nested `import all`s. -/
|
|
|
|
#check priv
|
|
|
|
#check { x := 1 : StructWithPrivateField }
|
|
|
|
#check (⟨1⟩ : StructWithPrivateField)
|