A simple declaration exporter for Lean 4 using the Lean 3 export format

How to Run

$ lake exe lean4export <mods> [-- <decls>]

This exports the contents of the given Lean modules, looked up in the core library or LEAN_PATH (as e.g. initialized by an outer lake env) and their transitive dependencies. A specific list of declarations to be exported from these modules can be given after a separating --.

Format Extensions

The following commands have been added to represent new features of the Lean 4 type system.

<eidx'> #EJ <nidx> <integer> <eidx>

A primitive projection of the <integer>-nth field of a value <eidx> of the record type <nidx>. Example: the primitive projection corresponding to Prod.snd of the innermost bound variable

1 #NS 0 Prod
0 #EV 0
1 #EJ 1 1 0

<eidx'> #ELN <integer>
<eidx'> #ELS <hexhex>*

Primitive literals of type Nat and String (encoded as a sequence of UTF-8 bytes in hexadecimal), respectively. Examples:

0 #ELN 1000000000000000
1 #ELS 68 69  # "hi"

<eidx'> #EZ <nidx> <eidx_1> <eidx_2> <eidx_3>

A binding let <nidx> : <eidx_1> := <eidx_2>; <eidx_3>. Already supported by the Lean 3 export format, but not documented. Example: the encoding of let x : Nat := Nat.zero; x is

1 #NS 0 x
2 #NS 0 Nat
0 #EC 2 
3 #NS 2 zero
1 #EC 3 
2 #EV 0
3 #EZ 1 0 1 2