learn how to write fully elaborated terms ?

Stream: general

[TongKe Xue]

https://leanprover-community.github.io/lean4-metaprogramming-book/main/02_overview.html talks about 'Fully Elaborated Terms'

Is there a tutorial / reference / set of exercises I can go through to learn how to write 'Fully Elaborated Terms' ?

I fully understand (1) this is not normally used, (2) this is going to be verbose/tedious, (3) typically this is some low level thing the elaborator/compiler emits, (4) humans are not meant to write at this level.

Purely out of intellectual curiosity, I'm curious what fully elaborated terms look like, how to manually construct them, (and what trusted kernels like nanoda_lib verify).

What is the best reading material / written exercises to go through to understand Fully Elaborated Terms ?

Thanks!

[Aaron Liu]

Where does it mention fully elaborated terms?

[TongKe Xue]

Maybe I am using the wrong terminology. I am referring to the structure that:

1. happens after the "elaboration" step (in the diagram) and
2. is fed directly into the "trusted lean4 kernel checker"

[Aaron Liu]

Oh you mean the docs#Lean.Expr

[Aaron Liu]

The next chapter in that book is all about them

[Aaron Liu]

and there's some exercises at the end

[Aaron Liu]

at the end of chapter 3, not at the end of the book

[TongKe Xue]

Is that the thing that goes into the "Kernel Check" at https://lean-lang.org/doc/reference/latest/Elaboration-and-Compilation/#:~:text=There%20are%20multiple%20kinds%20of,the%20state%20for%20subsequent%20commands. ?

[Aaron Liu]

yes it is

[TongKe Xue]

I'm 99% sure the answer to this is yes, but I just want to sanity check, as getting this wrong would be very bad

1. https://leanprover-community.github.io/lean4-metaprogramming-book/main/03_expressions.html
2. https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.Expr
3. https://github.com/ammkrn/nanoda_lib/blob/master/src/expr.rs#L20-L101

are the same thing; and in theory, I can take any Lean4 proof, push it to the point until we get a Lean.Expr out of it, write it, read it in nanoda_lib, and it should verify/pass the checker ?

[Aaron Liu]

I don't know about nanoda_lib, but everything else seems correct

[Niels Voss]

I think there a few caveats: Lean proofs can have metavariables while they are being assembled, and metavariable are a valid branch in Expr, but the kernel won't accept proofs with metavariables. Similarly, I'm not sure what the role of metadata is. Also, functions written using recursion will literally refer to themselves until some part of Lean removes it and replaces it with a recursor; if you get the expr before that happens somehow, I think the kernel will reject it

[Niels Voss]

So basically the finished proof will be an expr, but not all exprs are finished proofs

[Chris Bailey]

TongKe Xue said:

I'm 99% sure the answer to this is yes, but I just want to sanity check, as getting this wrong would be very bad

1. https://leanprover-community.github.io/lean4-metaprogramming-book/main/03_expressions.html
2. https://leanprover-community.github.io/mathlib4_docs/Lean/Expr.html#Lean.Expr
3. https://github.com/ammkrn/nanoda_lib/blob/master/src/expr.rs#L20-L101

are the same thing; and in theory, I can take any Lean4 proof, push it to the point until we get a Lean.Expr out of it, write it, read it in nanoda_lib, and it should verify/pass the checker ?

A notable difference is that nanoda_lib doesn't support mvar or mdata because they're not essential for type checking (reading more of the thread I see someone mentioned the mvar part).