Opaque in Lean 4 export

Stream: lean4

[Siddhartha Gadgil]

Continuing with my trepplein 4 adventures, the next failure I encounter seems to be that an opaque definition with an implementedBy seems to not be exported (at least before its use). Concretely, the bit which is needed is:

@[implemented_by TSyntaxArray.rawImpl]
opaque TSyntaxArray.raw (as : TSyntaxArray ks) : Array Syntax := Array.empty

and this is called by Lean.Syntax.mkApp.

@Sebastian Ullrich is this a bug in the exporter? Or is there another undocumented case in the export format? Or is it a problem with trepplein?

Meanwhile a partial update - I have implemented (following @Mario Carneiro) the nested inductives and they seem okay but bugs will only turn up in larger tests.

[Sebastian Ullrich]

I don't see how that attribute could affect the exporter but it's been some time since I looked at the code

[Siddhartha Gadgil]

There does seem to be a case where opaque is treated differently:
https://github.com/leanprover/lean4export/blob/f1d507ff8c8ba2df2316e78c0186a84c6791305f/Export.lean#L99

[Sebastian Ullrich]

Oh, that would certainly explain it

[Siddhartha Gadgil]

I have PRed the change. This fixes that error in trepplein but bugs remain (either created by mean or due to Lean 3 vs Lean 4).

[Siddhartha Gadgil]

Status update: the next bugs are because inequalities and operations on literal naturals need to be overridden.