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: Aug 03 2023 at 10:10 UTC