lean4-htt/src/shell
Sebastian Ullrich f6973be5e3 refactor: replace C++ import parser with Lean one
imports are now completely opaque to C++
2019-11-21 15:52:01 +01:00
..
CMakeLists.txt chore: use paths instead of indices for stdlib tests 2019-11-20 08:07:28 -08:00
lean.cpp refactor: replace C++ import parser with Lean one 2019-11-21 15:52:01 +01:00
lean_js.cpp feat(frontends/lean/vm_elaborator): recover from unknown identifiers 2019-02-07 14:16:28 +01:00
mk_lean_sh.sh