Lean Kernel C API

Stream: general

[graceinbound]

Hi there,

I’m building a small language with dependent types and would like to target the Lean 4 kernel for compilation. I know how to write a custom elaborator in Lean, but my language’s frontend will be implemented in C. Is there a stable C API for interacting with the Lean runtime / kernel? Any guidance or pointers to the best approach would be greatly appreciated.

Cheers!

[Arthur Paulino]

https://github.com/digama0/lean4lean is the best example I can think of for this