10 lines
412 B
Markdown
10 lines
412 B
Markdown
# Rust Call Lean
|
|
|
|
A tiny example of calling Lean's FFI from Rust with Nix.
|
|
|
|
This is based on:
|
|
* [Lean4 Reverse FFI](https://github.com/leanprover/lean4/tree/master/src/lake/examples/reverse-ffi)
|
|
* [Lean4 FFI](https://lean-lang.org/lean4/doc/dev/ffi.html#initialization)
|
|
* [Rustonomicon FFI](https://doc.rust-lang.org/nomicon/ffi.html)
|
|
* [Rust Bindgen](https://rust-lang.github.io/rust-bindgen/introduction.html)
|