Producing typing derivation trees for Lean

Stream: lean4

[Dylan Ede]

Is there any existing way of producing a derivation tree (i.e. proof of the typing judgement in terms of the typing rules) for a well-typed Lean expression? It seems that in the kernel at least, such trees are not explicitly constructed nor easily extractable. Does any external type checker produce such a tree/proof?

[Robin Arnez]

I did #metaprogramming / tactics > down to the axioms @ 💬 based on the axioms of #leantt once but the results are very long

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

We have a thing that does that in HoTTLean, see e.g. here (note that is on a PR branch). Our goals are a bit different than supporting all of Lean, e.g. we don't aim to support Prop anytime soon. We also don't support inductive types, but would like to.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Lean4Lean may also include this functionality? @Mario Carneiro

[Mario Carneiro]

No, that may happen on a branch somewhere but the official one doesn't. It does prove that a derivation exists though (modulo the sorries in the proof)

[Mario Carneiro]

the nearest equivalent is the one in HoTTLean

[Dylan Ede]

Thank you all, that is all very helpful.