how to hide definitions

Stream: lean4

[Jacob Prinz]

is there any way to hide definitions from outside modules in lean?
for example, inside the module i would have:

def a := 10
theorem fact : a > 5 := by repeat constructor

and then outside the module, i would have a : Nat and fact : a > 5, but it should be impossible to prove a = 10.

[Aaron Liu]

Maybe make a a public def and fact a public theorem but don't @[expose] the a?

[Aaron Liu]

still getting used to this module thing

[Jacob Prinz]

that doesn't seem to work, unless i'm misunderstanding how to use modules. i also tried having a second private version of a, and setting the public version to the private version, but this also didn't work. @[irreducible] doesn't seem to help either.

[Aaron Liu]

if it doesn't work then I have no more ideas

[Aaron Liu]

why doesn't it work?

[Jacob Prinz]

none of those strategies stop the proof of a = 10 going through in the other module, so it didn't get hidden.

[Aaron Liu]

Did you make it a module?

[Aaron Liu]

It be great if you gave some code so I can see what you're doing and maybe reproduce it

[Jacob Prinz]

i have a file test1.lean with

module
public def a := 10
public theorem fact : a > 5 := by repeat constructor

and a second file test2.lean with

import Project.test1
theorem test : a = 10 := by
  rfl

the proof goes though, which is what i'm trying to prevent

[Aaron Liu]

It only works if you make test2.lean also a module I think

[Aaron Liu]

otherwise you can't really hide anything

[Jacob Prinz]

thanks! that works