--only-export still gives a lot of exports

Stream: new members

[Thomas Brooks]

I'm trying to understand the simple export format described at https://github.com/leanprover-community/lean/blob/master/doc/export_format.md and want to look at basic examples. I made the file examples.lean containing:

constant f: Type

And when I run lean --export=exported --only-export=f examples.lean I expect to get a file with just a couple lines in it. Instead I get:

1 #NS 0 u
2 #NS 0 eq
3 #NS 0 α
1 #UP 1
0 #ES 1
4 #NS 0 a
1 #EV 0
2 #EV 1
3 #ES 0
4 #EP #BD 4 2 3
5 #EP #BD 4 1 4
6 #EP #BI 3 0 5
5 #NS 2 refl
7 #EC 2 1
8 #EA 7 2
9 #EA 8 1
10 #EA 9 1
11 #EP #BD 4 1 10
12 #EP #BI 3 0 11
#IND 2 2 6 1 5 12 1
#QUOT
6 #NS 0 f
2 #US 0
13 #ES 2
#AX 6 13
7 #NS 0 sum
#INFIX 7 30  ⊕
8 #NS 0 has_mem
9 #NS 8 mem
#INFIX 9 50  ∈
#INFIX 2 50  =
10 #NS 0 has_lt
11 #NS 10 lt
#INFIX 11 50  <
12 #NS 0 has_mul
13 #NS 12 mul
#INFIX 13 70  *
14 #NS 0 interaction_monad_bind
... to 183 lines total ...

While this gives much less than if I had not used --only-export, this clearly contains a lot more than I expected, like definitions of operators that aren't needed. Is there any way to reduce this further? I think my definition is the line that says #AX 6 13, so can I safely ignore everything below it? (Would that be true in more complicated examples too?)

[Alex J. Best]

If you add prelude at the top of your file what happens? This will not import everything in the lean init folder, which by default is imported in all files

[Thomas Brooks]

Thank you, that does the trick!