Leonardo de Moura
3218f91e35
feat(frontends/lean): add support for character literals
2016-07-18 14:07:10 -04:00
Leonardo de Moura
f34e84dacb
feat(frontends/lean/parser): cute binders
2016-07-08 07:50:58 -07:00
Leonardo de Moura
58569b82d3
refactor(frontends/lean,library,library/tactic): move type_context_cache_helper to type_context module
2016-06-30 12:03:40 +01:00
Leonardo de Moura
1a5756661f
refactor(frontends/lean,library): move scope_pos_info_provider to library
2016-06-30 10:19:35 +01:00
Leonardo de Moura
bb70fbbd48
refactor(frontends/lean): simplify elaborator_context
2016-06-29 16:56:19 +01:00
Leonardo de Moura
ccc65c6171
refactor(frontends/lean): add thread local parser_pos_provider
2016-06-29 16:09:06 +01:00
Leonardo de Moura
f3803c6ee4
refactor(frontends/lean/elaborator_context): remove io_state from elaborator_context
2016-06-27 06:29:54 +01:00
Leonardo de Moura
2ea8b26c4f
refactor(library/io_state): move get_global_ios to io_state module
2016-06-25 20:59:52 -07:00
Leonardo de Moura
77286e6abb
fix(frontends/lean): replay exported decls in imported files
2016-06-25 12:13:36 -07:00
Leonardo de Moura
586baa4118
feat(library,frontends/lean): support for quoted expressions in the VM, compiler and frontend
...
TODO: invoke elaborator at tactic.to_expr
2016-06-15 16:06:39 -07:00
Leonardo de Moura
3996f9db4d
feat(frontends/lean): add ( token and remove token
2016-06-15 13:22:31 -07:00
Leonardo de Moura
5459e9ad8a
chore(frontends/lean): remove dead code
2016-06-13 10:42:38 -07:00
Leonardo de Moura
b54203f6b3
feat(frontends/lean): parse by-expression
2016-06-13 10:25:26 -07:00
Leonardo de Moura
d302514933
chore(frontends/lean): remove tactic notation
2016-06-10 18:29:41 -07:00
Leonardo de Moura
e7b47a504e
feat(frontends/lean): add meta_definition and meta_constant commands
2016-06-01 09:12:41 -07:00
Leonardo de Moura
6a9e5079c9
feat(library,frontends/lean/pp): add support for new string encoding
2016-05-24 16:20:43 -07:00
Leonardo de Moura
fdea718d9d
chore(frontends/lean): remove all #include "library/tactic.*" from frontends/lean
2016-04-25 15:41:12 -07:00
Leonardo de Moura
d88098f38d
chore(frontends/lean): remove some of the tactic support
2016-04-25 15:26:56 -07:00
Leonardo de Moura
d66406a1f4
feat(frontends/lean): add #elab command for testing new elaborator
2016-04-05 17:03:23 -07:00
Leonardo de Moura
03809e7973
refactor(frontends/lean): elaborator_context
2016-04-05 16:19:06 -07:00
Leonardo de Moura
a1bc662eca
dev(frontends/lean/parser): add local_context
2016-03-30 16:33:17 -07:00
Leonardo de Moura
06ef0ad7be
refactor(frontends/lean): add local_level_decls
...
Remark: the template local_decls will be deleted in the future.
The instances local_expr_decls will be replace by local_context.
2016-03-30 15:47:32 -07:00
Leonardo de Moura
c4f25cf15b
refactor(frontends/lean): rename elaborate methods
2016-03-30 15:05:24 -07:00
Leonardo de Moura
75549bafd7
refactor(frontends/lean/elaborator): rename elaborator to old_elaborator
2016-03-30 14:59:18 -07:00
Leonardo de Moura
eaac6ba721
chore(library/type_context): rename default_type_context to legacy_type_context and move it to different file
2016-03-04 10:26:50 -08:00
Leonardo de Moura
3c878ecd01
feat(kernel): add let-expressions to the kernel
...
The frontend is still using the old "let-expression macros".
We will use the new let-expressions to implement the new tactic framework.
2016-02-29 16:40:17 -08:00
Leonardo de Moura
f54963bc3e
refactor(library/tactic/expr_to_tactic): remove 'by_plus' support
2016-02-29 13:50:05 -08:00
Leonardo de Moura
7d61f640f6
refactor(*): add abstract_type_context class
2016-02-26 14:17:34 -08:00
Leonardo de Moura
c9e9fee76a
refactor(*): remove name_generator and use simpler mk_fresh_name
2016-02-11 18:05:57 -08:00
Leonardo de Moura
9cbda49297
chore(frontends/lean): remove script blocks
2016-02-11 17:26:44 -08:00
Leonardo de Moura
f67181baf3
chore(*): remove support for Lua
2016-02-11 17:17:55 -08:00
Leonardo de Moura
b92416d66c
refactor(library/error_handling): move error_handling to library main dir
2015-12-29 15:31:40 -08:00
Leonardo de Moura
cac10aa728
fix(frontends/lean/parser): allow '...' token to be used in imports
...
Before this commit, we could not write
import ...foo.b
We had to write
import .. .foo.b
or
import . ..foo.b
2015-12-28 09:08:18 -08:00
Leonardo de Moura
61ecf018e9
feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ...
2015-12-17 12:18:32 -08:00
Leonardo de Moura
2502039a5c
fix(frontends/lean/parser): tactic notation that may take numerical parameters
2015-12-17 11:27:31 -08:00
Leonardo de Moura
727a4f5a3a
feat(library/tactic/intros_tactic): use '_' to say that some names are irrelevant in the intro tactic
...
See #695
2015-12-13 16:47:31 -08:00
Leonardo de Moura
20de22a8ad
feat(frontends/lean): automatically include anonymous instance implicit variables/parameters (whenever their parameters have been included)
2015-12-13 13:20:54 -08:00
Leonardo de Moura
a9b567296c
feat(frontends/lean/parser): add anonymous inst implicit name generator
2015-12-13 11:46:48 -08:00
Leonardo de Moura
d26a83da02
feat(frontends/lean/parser): allow anonymous instance implicit arguments
2015-12-13 11:46:48 -08:00
Leonardo de Moura
cf61adc5d5
feat(frontends/lean): identifiers starting with '_' are now reserved
2015-12-10 22:32:03 -08:00
Leonardo de Moura
1abaa9eb71
fix(frontends/lean/parser): fixes #858
2015-12-10 10:31:14 -08:00
Leonardo de Moura
e5a6bc5b85
feat(library/blast/simplifier/simplifier): move to new tracing framework
2015-12-08 12:59:30 -08:00
Leonardo de Moura
6b1469264d
feat(library/trace): add new tracing infrastructure
2015-12-08 11:58:03 -08:00
Leonardo de Moura
f78e57fd52
feat(shell,frontends/lean): add command line option --dir
...
See #821
See #788
2015-11-19 08:34:23 -08:00
Leonardo de Moura
c361fc1f6f
fix(frontends/lean/parser): method for parsing decimals
...
"division" has been renamed to "div"
2015-11-08 14:04:59 -08:00
Leonardo de Moura
b7e79dea29
fix(frontends/lean/parser): bug in parse_double
2015-11-08 14:04:56 -08:00
Leonardo de Moura
b777375469
fix(frontends/lean/parser): decimals
2015-11-08 14:04:56 -08:00
Leonardo de Moura
d1e111fd6c
fix(hott,frontends/lean,library,library/tactic): make sure we can still compile the HoTT library
2015-11-08 14:04:55 -08:00
Leonardo de Moura
8ee214f133
checkpoint: new numeral encoding
2015-11-08 14:04:55 -08:00
Leonardo de Moura
a618bd7d6c
refactor(library): use type classes for encoding all arithmetic operations
...
Before this commit we were using overloading for concrete structures and
type classes for abstract ones.
This is the first of series of commits that implement this modification
2015-11-08 14:04:54 -08:00
