Parameters across multiple files

Stream: general

[Bolton Bailey]

I think the answer to this is probably no, but I'll ask anyway.

I am currently dealing with a ~600 line file with many uses of parameter. I would like to be able to split the file up into different parts, but I run into the problem of the parameters I define in the first chunk not being usable in the second chunk. Is there any way to get parameters to persist across files?

[Mario Carneiro]

No. But, you can get most of the same effect by using local notations, which you can put at the top of each file:

local notation `thm1` := thm1 x y z
local notation `thm2` := thm2 x y z