michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
6227 commits 3 branches 0 tags 28 MiB
Commit graph

1439 commits

Author SHA1 Message Date
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
3e87f09d78 feat(library/tactic/induction_tactic): add support for user-defined recursors that contain parameters that should be synthesized by type class resolution 2015-05-19 15:33:46 -07:00
Leonardo de Moura
937d6ac7b6 fix(frontends/lean/pp): print notation produces incorrect output 
fixes #604
 2015-05-19 09:57:13 -07:00
Leonardo de Moura
e1c2340db2 fix(frontends/lean): consistent behavior for protected declarations 
see https://github.com/leanprover/lean/issues/604#issuecomment-103265608

closes #609
 2015-05-18 22:35:18 -07:00
Leonardo de Moura
d8bd3c21b5 feat(frontends/lean/builtin_cmds): display "protected" for protected declarations in the print command 2015-05-18 17:19:34 -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
c61c049152 feat(library/user_recursors): generalize acceptable use-defined recursors 
see issue #492
 2015-05-18 14:21:10 -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
Leonardo de Moura
7f8afcf04b fix(frontends/lean/builtin_exprs): bug in 'using' expressions 2015-05-14 17:17:48 -07:00
Leonardo de Moura
cbcaf5a48e fix(frontends/lean/scanner): block comments 
fixes #600
 2015-05-13 22:14:28 -07:00
Leonardo de Moura
ed388b00f1 fix(frontends/lean/builtin_cmds): issue #597 2015-05-13 15:34:34 -07:00
Leonardo de Moura
11fbee269b fix(frontends/lean/parser): must save state of name_generator in parser snapshot 
To provide typing and auto-completion information, we create a
background process by starting lean with the option --server.
In "server" mode, we create snapshots of the parser state.
The idea is to be able to quickly reprocess a file when the user makes a
modification. This commit fixes a bug in the snapshot operation.
It was not saving in the snapshots the unique name generator used by the parser.
By creating a fresh name generator, we may accidentally
assign the same internal name to two different constants.
This bug triggered the crash described in issue #593.

This commit fixes the test in the comment
https://github.com/leanprover/lean/issues/593#issuecomment-101768484

This commit also adds a smaller version of the problem to the test suite
 2015-05-13 12:28:23 -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
f403ea984b feat(frontends/lean): add 'print [recursor]' command for debugging purposes 2015-05-12 15:48:24 -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
3d8586088b fix(frontends/lean/elaborator): problem with 'calc' proofs discussed at issue #592 2015-05-11 13:22:39 -07:00
Leonardo de Moura
299fd5c919 feat(frontends/lean/pp): pp inaccessible patterns 2015-05-10 11:08:02 -07:00
Leonardo de Moura
e9c8de7bdf feat(frontends/lean): remove unnecessary option 2015-05-09 11:49:55 -07:00
Leonardo de Moura
bd28396be0 feat(kernel): transparent theorems 
closes #576
 2015-05-09 11:42:29 -07:00
Leonardo de Moura
4e35afedcc feat(frontends/lean): rename 'wait' to 'reveal' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2015-05-08 20:54:16 -07:00
Leonardo de Moura
f8e2f68ce0 feat(frontends/lean): add 'wait' command 
This commit also fixes several problems with -j option (parallel
compilation). The .olean files were not missing data when -j was used

see issue #576
 2015-05-08 20:05:21 -07:00
Leonardo de Moura
e6566e5814 fix(frontends/lean/parser): incorrect error message 2015-05-08 18:13:44 -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
cf7e60e5a6 refactor(kernel): remove "opaque" field from kernel declarations 
see issue #576
 2015-05-08 16:06:16 -07:00
Leonardo de Moura
57ea660963 refactor(*): start process for eliminating of opaque definitions from the kernel 
see issue #576
 2015-05-08 16:06:04 -07:00
Leonardo de Moura
061e26157e fix(kernel,library): make sure macros check relevant arguments when kernel is performing full type checking 2015-05-08 12:41:23 -07:00
Leonardo de Moura
12bad8794b feat(frontends/lean/pp): use 'assert' instead of 'have ... [visible]' 2015-05-08 10:02:15 -07:00
Leonardo de Moura
0b57f7d00a refactor(library/tactic): refine interface between tactic and proof-term modes 
Some constraints were being lost with the previous interface.
This is why we had a workaround in fintype.lean.

We can also remove some hacks we have used in the past.
 2015-05-07 18:02:51 -07:00
Leonardo de Moura
f6a1d1c864 fix(frontends/lean/parser): fixes #584 2015-05-07 14:24:30 -07:00
Leonardo de Moura
aff9257c72 feat(frontends/lean): allow → to be used in calc proofs 
see issue #586
 2015-05-07 12:28:47 -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
5fdf140096 refactor(frontends/lean): simplify local_decls data-structure 
This is the first step for fixing #584
 2015-05-07 11:10:15 -07:00
Leonardo de Moura
e0b7017435 feat(frontends/lean): make sure the proof state bit "report errors" is 
set in the beginning of each begin-end element

see discussion at #583
 2015-05-07 09:43:39 -07:00
Leonardo de Moura
5798ac43de fix(frontends/lean/structure_cmd): 'structure' command must set unfold-c attribute for auxiliary recursors 
fixes #582
 2015-05-07 09:09:07 -07:00
Leonardo de Moura
171530d5cc fix(frontends/lean/notation_cmd): fixes #585 2015-05-07 08:36:37 -07:00
Leonardo de Moura
613281d622 fix(frontends/lean/builtin_exprs): bug in new 'obtain' expression 2015-05-06 10:01:24 -07:00
Leonardo de Moura
26c662accd feat(frontends/lean/builtin_exprs): improve new 'obtain' expression 2015-05-06 09:56:57 -07:00
Leonardo de Moura
4cdfc9ee84 feat(frontends/lean/pp): add pretty printing functions for debugging purposes 2015-05-06 07:50:56 -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
616f49c2e4 feat(frontends/lean): improved 'obtains' expression 2015-05-05 18:30:16 -07:00
Leonardo de Moura
8aefcc182e feat(frontends/lean/parser): add 'parse_simple_binders' 2015-05-05 18:30:16 -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
87aaf373f4 fix(frontends/lean): fix '#' override notation on the left-hand-side of recursive equations (and match-expressions) 2015-05-03 21:08:09 -07:00
Leonardo de Moura
441f1f9fe2 feat(frontends/lean): import error message for "unknown" tactics when parsing 2015-05-02 18:57:58 -07:00
Leonardo de Moura
118189eaac fix(frontends/lean/elaborator): bug in translation function 
This commit fixes the bug reported in the lean discussion list:
https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc
 2015-05-02 18:05:07 -07:00
Leonardo de Moura
8c107d6936 fix(frontends/lean/builtin_cmds): bug in export command 
Cause: we have two different tokes to represent declarations: [decls] and [declarations]

fixes #568
 2015-05-02 16:01:25 -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
ce5ef5a6cc feat(frontends/lean): improver parser for tactics of the form 'tac_name <expr> with <ids*>' 2015-05-01 13:06:11 -07:00