Leonardo de Moura 7260ac91ed feat(library/init/compiler/ir): declare new IR in Lean ... Next steps: - Implement more validators (e.g., blockid validator, type checker). - Implement C++ code generator (in Lean). We can use it for testing the new lean_obj module implemented in C++. - Implement interpreter (in C++) for sanity checking. - Implement LLVM IR generator (in Lean). It just outputs a text file using LLVM syntax. After, we are confident we are generating valid LLVM IR, we can try to link LLVM with Lean.		2018-04-20 18:27:13 -07:00
..
ir.lean	feat(library/init/compiler/ir): declare new IR in Lean	2018-04-20 18:27:13 -07:00