Zulip Chat Archive

Stream: general

Topic: Parameters across multiple files

Bolton Bailey (Jun 24 2021 at 23:52):

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 (Jun 25 2021 at 00:20):

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

Last updated: Dec 20 2023 at 11:08 UTC