569e46033b
This PR adjusts the experimental module system to not export any private declarations from modules. Fixes #5002
21 lines
330 B
Text
21 lines
330 B
Text
module
|
|
|
|
/-! Module docstring -/
|
|
|
|
/-- A definition. -/
|
|
def f := 1
|
|
|
|
/-- A theorem. -/
|
|
theorem t : f = 1 := sorry
|
|
|
|
theorem trfl : f = 1 := rfl
|
|
|
|
@[expose] def fexp := 1
|
|
|
|
private def priv := 2
|
|
|
|
/-! Private decls should not be accessible in exported contexts. -/
|
|
|
|
/-- error: unknown identifier 'priv' -/
|
|
#guard_msgs in
|
|
abbrev h := priv
|