Export contains tag #EZ that is not documented

[huma23]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Just a documentation issue:
The low level format export contains the tag #EZ which is not covered in the export.md file.
For example:
21786 #EZ 479 21761 21769 21785

Guess the notation of this tag would be:
<eidx'> #EZ <eidx_1> <eidx_2> <eidx_3> <eidx_4>

But I'm not sure what it exactly means. Could you add some information for this expression to the export.md file?

Thanks.

Steps to Reproduce

1. cd lean/library
2. lean --export=export.out --recursive
3. find #EZ in the export.out

Expected behavior: [What you expect to happen]

Actual behavior: [What actually happens]

Reproduces how often: [What percentage of the time does it reproduce?]

Versions

Lean (version 3.4.1, commit 17fe3de, Release)
Ubuntu 18.04.1 LTS

Additional Information

[fpvandoorn]

Reverse engineering from the trepplein source code this is a let-binder. The notation tag would be <eidx'> #EZ <nidx> <eidx_1> <eidx_2> <eidx_3> and the line n #EZ x A v e would stand for the expression let x : A := v in e.
I will let anyone who actually knows this for certain change the export_format.md file.