| .. |
|
CMakeLists.txt
|
feat(frontends/lean): Scopes in the default Lean frontend
|
2013-12-18 17:40:21 -08:00 |
|
coercion.h
|
Rename lean frontend files. The prefix lean_ is not necessary anymore.
|
2013-09-12 20:09:35 -07:00 |
|
environment_scope.cpp
|
feat(frontends/lean): Scopes in the default Lean frontend
|
2013-12-18 17:40:21 -08:00 |
|
environment_scope.h
|
feat(frontends/lean): Scopes in the default Lean frontend
|
2013-12-18 17:40:21 -08:00 |
|
frontend.cpp
|
refactor(kernel/type_checker): combine type_checker and type_inferer into a single class, and avoid code duplication
|
2013-12-22 11:51:38 -08:00 |
|
frontend.h
|
feat(frontends/lean): hide builtin object in the 'Show Environment' command
|
2013-12-19 14:00:58 -08:00 |
|
frontend_elaborator.cpp
|
feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions
|
2013-12-22 17:57:51 -08:00 |
|
frontend_elaborator.h
|
feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables
|
2013-12-20 22:00:50 -08:00 |
|
notation.cpp
|
refactor(library/cast): replace cast semantic attachment with axioms, add heterogeneous symmetry axiom
|
2013-12-21 18:23:37 -08:00 |
|
notation.h
|
fix(frontends/lean/pp): make sure pp and parser are using the same precedences
|
2013-12-19 12:46:14 -08:00 |
|
operator_info.cpp
|
chore(util/rc): remove unnecessary argument from LEAN_COPY_REF and LEAN_MOVE_REF macros
|
2013-12-13 15:01:24 -08:00 |
|
operator_info.h
|
refactor(library/io_state): simplify regular/diagnostic
|
2013-12-10 13:09:35 -08:00 |
|
parser.cpp
|
fix(frontends/lean/parser): readline compilation problem on Fedora19
|
2013-12-23 13:12:39 -08:00 |
|
parser.h
|
feat(frontends/lean): macro definition using Lua
|
2013-12-19 19:08:10 -08:00 |
|
pp.cpp
|
feat(frontends/lean): improve error messages when elaborator cannot instantiate all metavariables
|
2013-12-20 22:00:50 -08:00 |
|
pp.h
|
refactor(kernel/environment): add ro_environment
|
2013-12-12 16:48:34 -08:00 |
|
register_module.cpp
|
feat(frontends/lean): macro definition using Lua
|
2013-12-19 19:08:10 -08:00 |
|
register_module.h
|
refactor(frontends/lua): rename leanlua_state to script_state, and move it to util
|
2013-11-27 14:57:36 -08:00 |
|
scanner.cpp
|
feat(frontends/lean): simplify explicit version names
|
2013-12-21 17:05:25 -08:00 |
|
scanner.h
|
feat(frontends/lean): allow 'tactic hints' to be associated with 'holes'
|
2013-12-06 14:49:39 -08:00 |
