Leonardo de Moura
|
d395a54165
|
feat(frontends/lean): add '[forward]' annotation
|
2015-11-25 17:44:58 -08:00 |
|
Leonardo de Moura
|
a2f43212d6
|
feat(frontends/lean): add '[no_pattern]' attribute
|
2015-11-24 18:48:22 -08:00 |
|
Daniel Selsam
|
413989afd6
|
feat(library/blast/backward): backward chaining strategy
|
2015-11-18 17:48:39 -08:00 |
|
Leonardo de Moura
|
1d670e3193
|
feat(frontends/lean): support for '@@' -- the partial explicit operator
|
2015-11-08 14:05:00 -08:00 |
|
Leonardo de Moura
|
744d1cba3d
|
feat(library,hott,frontends/lean): avoid keywords with hyphen
|
2015-11-08 14:04:54 -08:00 |
|
Leonardo de Moura
|
28a5ca5809
|
fix(frontends/lean): fixes #830
|
2015-09-18 07:51:02 -07:00 |
|
Leonardo de Moura
|
3a72cd9621
|
fix(frontends/lean): rename multiword keyword "suffices to show" to "suffices"
|
2015-08-18 17:57:53 -07:00 |
|
Leonardo de Moura
|
3ce8c5d6f7
|
feat(frontends/lean): add "suffices to show A, from B, C" construct
|
2015-08-18 17:04:38 -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
|
308af87b69
|
feat(library): add 'noncomputable' keyword for the standard library
|
2015-07-28 21:56:35 -07:00 |
|
Leonardo de Moura
|
946308b187
|
feat(frontends/lean): allow anonymous 'have'-expressions in tactic mode
|
2015-07-23 18:52:59 -07:00 |
|
Leonardo de Moura
|
18dd7c13f9
|
feat(frontends/lean): add '[congr]' attribute
|
2015-07-22 17:21:47 -07:00 |
|
Leonardo de Moura
|
092c8d05b9
|
feat(frontends/lean,library): rename '[rewrite]' to '[simp]'
|
2015-07-22 09:01:42 -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
|
92f8eb173b
|
feat(frontends/lean): use 'this' as the name for anonymous 'have'-expression
|
2015-07-18 13:36:05 -05:00 |
|
Leonardo de Moura
|
4b1b3e277f
|
feat(frontends/lean): rename '[unfold-c]' to '[unfold]' and '[unfold-f]' to '[unfold-full]'
see issue #693
|
2015-07-07 16:37:06 -07:00 |
|
Leonardo de Moura
|
3215af3926
|
feat(frontends/lean): add '[trans-instance]' attribute
see issue #666
|
2015-06-27 14:07:29 -07:00 |
|
Leonardo de Moura
|
0fbc944cdd
|
feat(frontends/lean): add '[rewrite]' attribute
|
2015-06-01 17:58:24 -07:00 |
|
Leonardo de Moura
|
8ce992b077
|
feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode
|
2015-05-19 16:26:02 -07:00 |
|
Leonardo de Moura
|
5f628d5080
|
feat(frontends/lean/builtin_exprs): allow 'calc' expressions to be used in tactic mode
|
2015-05-19 15:54:49 -07:00 |
|
Leonardo de Moura
|
c61c049152
|
feat(library/user_recursors): generalize acceptable use-defined recursors
see issue #492
|
2015-05-18 14:21:10 -07:00 |
|
Leonardo de Moura
|
2014a4a672
|
chore(script/gen_tokens_cpp): mark automatically generated global variables as static
|
2015-05-12 17:15:31 -07:00 |
|
Leonardo de Moura
|
358afcf42c
|
fix(script/gen_tokens_cpp): automatically generated header
|
2015-05-12 17:11:27 -07:00 |
|
Leonardo de Moura
|
c60f11ab05
|
refactor(frontends/lean): add script for automatically generating tokens.h and tokens.cpp
|
2015-05-12 17:07:08 -07:00 |
|
Leonardo de Moura
|
750f6d5a43
|
feat(library,frontends/lean): validate user defined recursors and add attribute to mark them
see issue #492
The user-defined recursors will also be used to implement the blast tactic
|
2015-05-12 15:48:01 -07:00 |
|
Leonardo de Moura
|
e9c8de7bdf
|
feat(frontends/lean): remove unnecessary option
|
2015-05-09 11:49:55 -07:00 |
|
Leonardo de Moura
|
e59456c19f
|
feat(frontends/lean): remove 'opaque' keyword
see issue #576
|
2015-05-08 16:45:13 -07:00 |
|
Leonardo de Moura
|
b03266be70
|
feat(library/normalize,frontends/lean): rename '[unfold-m]' hint to '[constructor]', and allow it to be attached to constants
closes #587
|
2015-05-07 12:00:34 -07:00 |
|
Leonardo de Moura
|
7cd444882c
|
feat(frontends/lean): add 'begin+' and 'by+' that enter tactic mode with the whole context visible
|
2015-05-05 18:47:25 -07:00 |
|
Leonardo de Moura
|
6571c47353
|
feat(library/normalize): add '[unfold-m]' hint
See issue #496
|
2015-05-04 14:23:04 -07:00 |
|
Leonardo de Moura
|
cd17618f4a
|
refactor(library): replace 'calc_trans', 'calc_symm', 'calc_refl' and 'calc_subst' commands with attributes '[symm]', '[refl]', '[trans]' and '[subst]'
These attributes are used by the calc command.
They will also be used by tactics such as 'reflexivity', 'symmetry' and
'transitivity'.
See issue #500
|
2015-05-02 15:15:35 -07:00 |
|
Leonardo de Moura
|
1a28a3c36f
|
feat(frontends/lean): add 'print inductive' command
|
2015-04-29 15:22:10 -07:00 |
|
Leonardo de Moura
|
60e320fd79
|
feat(frontends/lean): protected constants and axioms
fixes #527
|
2015-04-19 17:45:58 -07:00 |
|
Leonardo de Moura
|
d731a4ab13
|
feat(library/normalize): add '[unfold-f]' hint
closes #497
|
2015-04-05 03:00:13 -07:00 |
|
Leonardo de Moura
|
9b577a7b3e
|
feat(frontends/lean): add 'migrate' command
|
2015-03-14 21:48:00 -07:00 |
|
Leonardo de Moura
|
bd8c4315f1
|
feat(frontends/lean): allow 'match-with' to be used in tactics without prefixing it with 'exact'
|
2015-03-06 15:49:31 -08:00 |
|
Leonardo de Moura
|
3b721fe675
|
feat(frontends/lean): add missing 'help' command
|
2015-03-06 13:56:20 -08:00 |
|
Leonardo de Moura
|
368f9d347e
|
refactor(frontends/lean): approach used to parse tactics
The previous approach was too fragile
TODO: we should add separate parsing tables for tactics
|
2015-03-05 18:11:21 -08:00 |
|
Leonardo de Moura
|
8e9ccf8b6f
|
chore(frontends/lean): remove 'dead' tokens
|
2015-03-05 14:37:29 -08:00 |
|
Leonardo de Moura
|
e4060a5614
|
feat(frontends/lean): do not force user to type the function name in the left-hand-side of recursive equations
|
2015-03-05 12:08:36 -08:00 |
|
Leonardo de Moura
|
abd238aef0
|
feat(*): add [quasireducible] attribute
|
2015-03-04 22:12:49 -08:00 |
|
Leonardo de Moura
|
11aad4449b
|
feat(frontends/lean): add '[semireducible]' attribute
This commit also renames the elements of reducible_status.
The idea is to use in the C++ implementation the same names used in the
Lean front-end.
|
2015-03-03 10:48:36 -08:00 |
|
Leonardo de Moura
|
c04c610b7b
|
feat(frontends/lean): add 'assert H : A, ...' as notation for 'have H [visible] : A, ...'
|
2015-02-25 14:30:42 -08:00 |
|
Leonardo de Moura
|
9d1cd073c5
|
feat(frontends/lean): add 'print metaclasses' command
|
2015-02-11 10:13:20 -08:00 |
|
Leonardo de Moura
|
565cd835af
|
feat(frontends/lean): add 'abbreviation' command
|
2015-02-10 17:31:40 -08:00 |
|
Leonardo de Moura
|
c04c0e8381
|
refactor(*): remove transparent_scope hack, replace [strict] with [all-transparent] annotation
|
2015-02-07 15:19:41 -08:00 |
|
Leonardo de Moura
|
1e8a975daa
|
feat(frontends/lean): extend parser: rewrite "fold" step
|
2015-02-06 15:22:34 -08:00 |
|
Leonardo de Moura
|
bc95f09828
|
feat(frontends/lean/decl_cmds): allow user to specify unfold-c hint
|
2015-02-06 12:56:52 -08:00 |
|
Leonardo de Moura
|
dfad24e3f5
|
feat(frontends/lean): polish rewrite tactic notation
|
2015-02-05 10:15:58 -08:00 |
|
Leonardo de Moura
|
08dcc9e2fc
|
feat(frontends/lean/parse_rewrite_tactic): polish rewrite tactic notation
|
2015-02-04 19:19:19 -08:00 |
|