e2f757d5a7
This PR adds support for the following import variants to the experimental module system: * `private import`: Makes the imported constants available only in non-exported contexts such as proofs. In particular, the import will not be loaded, or required to exist at all, when the current module is imported into other modules. * `import all`: Makes non-exported information such as proofs of the imported module available in non-exported contexts in the current module. Main purpose is to allow for reasoning about imported definitions when they would otherwise be opaque. TODO: adjust name resolution so that imported `private` decls are accessible through syntax. They can be combined into `private import all`, which will likely be the most common usage of `import all`.
22 lines
380 B
Text
22 lines
380 B
Text
module
|
|
|
|
private import Module.Basic
|
|
|
|
/-! `private import` should allow only private access to imported decls. -/
|
|
|
|
/--
|
|
error: type mismatch
|
|
f
|
|
has type
|
|
Nat : Type
|
|
but is expected to have type
|
|
True : Prop
|
|
-/
|
|
#guard_msgs in
|
|
theorem g : True := f
|
|
|
|
/- FIXME: visibility for def bodies is wrong
|
|
/-- error: unknown identifier 'f' -/
|
|
#guard_msgs in
|
|
@[reducible] def h : True := f
|
|
-/
|