Leonardo de Moura
|
3a5f6f2e64
|
feat(frontends/lean/builtin_cmds): improve output produced by #elab command, use kernel type checker to check elaboration result
|
2016-07-27 15:29:25 -07:00 |
|
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
|
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
|
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
|
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
|
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
|
f67181baf3
|
chore(*): remove support for Lua
|
2016-02-11 17:17:55 -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
|
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
|
3f9549485f
|
feat(frontends/lean/parser): restore config options in the end of sections/namespaces
|
2015-12-09 11:24:37 -08:00 |
|
Leonardo de Moura
|
f84c6a6cfa
|
fix(library/blast,frontends/lean): handling pattern hints after unfolding
|
2015-12-02 22:52:55 -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
|
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
|
b07a364d2f
|
feat(frontends/lean/parser): process multiple parsing actions
closes #800
|
2015-08-17 09:42:10 -07:00 |
|
Leonardo de Moura
|
ea04414058
|
feat(frontends/lean): allow user to overload notation containing foldr/foldl and/or scoped expressions
see new tests for a summary of new features
see issue #800
|
2015-08-16 18:24:30 -07:00 |
|
Leonardo de Moura
|
602626803b
|
fix(frontends/lean/builtin_cmds): 'print axioms' and theorem queue
|
2015-08-11 21:08:45 -07:00 |
|
Leonardo de Moura
|
5d8d226640
|
fix(frontends/lean/parser): add support for decimals
Decimal numbers are notation for rationals.
If rat.of_num is not available, then an error is generated.
closes #793
|
2015-08-11 18:44:48 -07:00 |
|
Leonardo de Moura
|
cc4f18c062
|
feat(frontends/lean): add "--info" command line option for extracting identifier/keyword information
see issue #756
|
2015-07-30 10:18:03 -07:00 |
|
Leonardo de Moura
|
be61fb0566
|
feat(frontends/lean/elaborator): add "noncomputable theory" command, display "noncomputable" when printing definitions
When the command "noncomputable theory" is used, Lean will not sign an
error when a noncomputable definition is not marked as noncomputable
|
2015-07-29 17:54:35 -07:00 |
|
Leonardo de Moura
|
0bda39c8ac
|
feat(frontends/lean): check for noncomputability when moving theorems from theorem_queue to environment
|
2015-07-29 13:01:07 -07:00 |
|
Leonardo de Moura
|
cfa9412f96
|
fix(frontends/lean): "show goal" localization, add "position", support "by tactic"
|
2015-07-28 12:48:12 -07:00 |
|
Leonardo de Moura
|
68370d5c8e
|
feat(frontends/lean): process "show goal" command line option
|
2015-07-27 17:44:43 -07:00 |
|
Leonardo de Moura
|
cc396cba76
|
feat(frontends/lean): allow backticks in binder declarations
|
2015-07-22 13:54:47 -07:00 |
|
Leonardo de Moura
|
b9451549d1
|
feat(frontends/lean): add type notation for referencing hypotheses
|
2015-07-20 21:43:47 -07:00 |
|
Leonardo de Moura
|
f5c546e810
|
feat(frontends/lean/parse_simp_tactic): add simp tactic parser
|
2015-07-14 14:21:39 -04:00 |
|
Leonardo de Moura
|
cabe30ba71
|
feat(frontends/lean): allow user to assign priorities to notation declarations
|
2015-06-30 17:10:27 -07:00 |
|
Leonardo de Moura
|
8a85e4ee87
|
feat(frontends/lean/builtin_cmds): improve print <id> when <id> is a not yet revealed theorem
We add a remark saying the command `reveal <id>` should be used to
access `<id>` definition.
|
2015-06-13 12:12:22 -07:00 |
|
Leonardo de Moura
|
c53b96c8d3
|
feat(frontends/lean): print all options for overloaded identifier
closes #608
|
2015-05-18 17:14:17 -07:00 |
|
Leonardo de Moura
|
b1ece388a6
|
feat(frontends/lean,library/tactic/induction_tactic): improve induction tactic notation, expand induction tactic implementation
|
2015-05-18 09:25:07 -07:00 |
|