GitHub

To build and run:

lake build
cd build; mkdir debug; cd debug
cmake ../..
make -j
./main
./main2

Quick rebuild command from build/debug directory

pushd ../../; lake build; popd; make -j

Potentially set up LD_LIBRARY_PATH to have libleanshared.so available

export LD_LIBRARY_PATH=~/.elan/toolchains/leanprover--lean4---nightly/lib/lean

Name		Name	Last commit message	Last commit date
Latest commit History 5 Commits
CMakeLists.txt		CMakeLists.txt
Package.lean		Package.lean
lakefile.lean		lakefile.lean
lean-toolchain		lean-toolchain
main.cpp		main.cpp
main2.cpp		main2.cpp
plugin.cpp		plugin.cpp
plugin2.cpp		plugin2.cpp
readme.org		readme.org

Provide feedback