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

579 commits

Author SHA1 Message Date
Leonardo de Moura
d591c63840 feat(frontends/lean/decl_cmds): allow local coercions in contexts 
closes #525
 2015-04-04 15:25:07 -07:00
Leonardo de Moura
8c59f17605 feat(frontends/lean): 'using' expression without 'show' or 'have' 
closes #536
 2015-04-04 15:25:07 -07:00
Leonardo de Moura
4ec0e1b07c feat(frontends/lean): improve calc mode 
Now, it automatically supports transitivity of the form
    (R a b) -> (b = c) -> R a c
    (a = b) -> (R b c) -> R a c

closes #507
 2015-04-04 08:58:35 -07:00
Leonardo de Moura
1150b19598 perf(frontends/lean/elaborator): do not invoke recursive equation compiler when equations still contain metavariables 2015-04-02 23:37:33 -07:00
Leonardo de Moura
f8023403af test(tests/lean/run): add another simple test 2015-04-01 15:49:01 -07:00
Leonardo de Moura
0d66d19ba3 feat(tests/lean/run/finset): show that if A has decidable equality, then (finset A) also has it. 2015-04-01 13:19:16 -07:00
Leonardo de Moura
b960e123b1 feat(kernel): add experimental support for quotient types 2015-03-31 22:04:16 -07:00
Soonho Kong
8243ed6339 fix(test*.sh): allow spaces in filename 
fix #515
 2015-03-28 23:29:52 -04:00
Leonardo de Moura
75621df52b feat(frontends/lean): uniform notation for lists in tactics 
closes #504
 2015-03-27 17:54:48 -07:00
Leonardo de Moura
0c3fd7427e feat(frontends/lean): add syntax-sugar for fold 
closes #503
 2015-03-25 18:25:48 -07:00
Leonardo de Moura
f2b1752807 fix(frontends/lean/parser): add workaround for #461 2015-03-25 18:09:43 -07:00
Leonardo de Moura
b9e3c474c9 feat(library/tactic): add all_goals tactic 
closes #501
 2015-03-25 17:42:34 -07:00
Leonardo de Moura
a1f933886f fix(frontends/lean/structure_cmd): explicit universe levels for structures 
closes #490
 2015-03-25 16:10:30 -07:00
Leonardo de Moura
33d2e8d9d3 test(tests/lean/run): workaround for issue #505 2015-03-25 15:53:50 -07:00
Leonardo de Moura
bed0d6df6b fix(frontends/lean/elaborator): inaccessible over coercion 2015-03-13 23:04:45 -07:00
Leonardo de Moura
47a350d888 fix(library/tactic/inversion_tactic): missing condition for applying optimization 2015-03-12 09:11:36 -07:00
Leonardo de Moura
4c6b0dc0e5 fix(library/tactic/expr_to_tactic): tactic_expr_to_id did not take as_atomic annotation into account 
fixes #466
 2015-03-11 08:49:59 -07:00
Leonardo de Moura
4904f7657f test(tests/lean/run): add definition package tests 2015-03-09 08:42:21 -07:00
Leonardo de Moura
f966634910 feat(frontends/lean): nested dependent pattern matching 2015-03-06 19:18:08 -08:00
Leonardo de Moura
14ca2d407d test(tests/lean/run): add match-with nested in tactic test 2015-03-06 17:47:01 -08:00
Leonardo de Moura
1490bdad49 feat(frontends/lean): add version of 'exact' tactic (sexact) that enforces goal type during term elaboration 2015-03-06 17:34:45 -08: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
4edd7b9099 fix(library/definitional/equations): allow a function to be the result of a match-with term or recursive definition 2015-03-06 15:08:52 -08:00
Leonardo de Moura
f24d9e84fe feat(frontends/lean): add option 'max_memory' 
Default value is 512Mb
 2015-03-06 13:56:20 -08:00
Leonardo de Moura
3b721fe675 feat(frontends/lean): add missing 'help' command 2015-03-06 13:56:20 -08:00
Leonardo de Moura
daf36803c4 fix(frontends/lean/builtin_exprs): bug in 'using' construct 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
28487ede3b feat(frontends/lean/decl_cmds): allow 'empty' set of pattern matching equations 2015-03-05 14:37:29 -08:00
Leonardo de Moura
b73a931c70 fix(frontends/lean/elaborator): missing case 'no-equation' annotation 2015-03-05 14:37:29 -08:00
Leonardo de Moura
039afb4578 feat(frontends/lean): treat "proof t qed" as alias for "by exact t" 2015-03-05 11:12:39 -08:00
Leonardo de Moura
abd238aef0 feat(*): add [quasireducible] attribute 2015-03-04 22:12:49 -08:00
Leonardo de Moura
fa79b214b8 fix(frontends/lean): allow 'attribute <id> [priority ...]' 2015-03-03 16:17:32 -08:00
Leonardo de Moura
3b73e100dc test(tests/lean/run): add [priority] test using num.sub 2015-03-03 15:59:17 -08:00
Leonardo de Moura
efd096e85c feat(library/init/num): define sub and le for binary numerals 2015-03-03 15:55:16 -08:00
Leonardo de Moura
c772d7bf84 fix(frontends/lean/elaborator): unassigned metavariable when using nested begin-end blocks 
Closes #454
 2015-02-28 09:03:56 -08:00
Leonardo de Moura
cf56935b01 feat(frontends/lean): improve support for user defined tactics 2015-02-27 16:58:25 -08:00
Leonardo de Moura
5b736a2268 feat(frontends/lean): add support for empty match-with expressions 2015-02-26 16:36:15 -08:00
Leonardo de Moura
68110faa4d feat(frontends/lean/inductive_cmd): allow '|' in inductive datatype declarations 2015-02-25 17:00:10 -08:00
Leonardo de Moura
5ca52d81ec feat(frontends/lean): ML-like notation for match and recursive equations 2015-02-25 16:20:44 -08:00
Leonardo de Moura
3c24461e51 refactor(*): modify '|' binding power, use 'abs a' instead of '|a|', and '(a | b)' instead of 'a | b' 2015-02-25 15:18:21 -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
Jeremy Avigad
e555531eb6 feat(library/data/int/div): start on div for integers 2015-02-25 14:05:07 -08:00
Leonardo de Moura
96b54a8007 feat(frontends/lean/builtin_exprs): add 'have' notation in 'begin-end' blocks 
It is notation for the assert tactic.
 2015-02-25 14:04:17 -08:00
Leonardo de Moura
909ebfc5f1 feat(frontends/lean/elaborator): try coercions after each overload 
We try only the easy cases since the more general case is too expensive.

closes #444
 2015-02-24 17:41:20 -08:00
Leonardo de Moura
34c36648bb fix(frontends/lean/decl_cmds): constants command 
closes #445
 2015-02-24 16:27:13 -08:00
Leonardo de Moura
42289d4334 feat(library/tactic/class_instance_synth): create class instance synthesis subproblems only for arguments marked with the [] binder annotation 2015-02-24 16:12:39 -08:00
Leonardo de Moura
1cd44e894b feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible 
closes #442
 2015-02-24 16:12:35 -08:00
Leonardo de Moura
1ff6446a63 feat(frontends/lean): nested begin-end blocks 2015-02-24 11:59:27 -08:00
Leonardo de Moura
dc2ac92846 fix(library/definitional/equations): use whnf on recursive definition arguments 
The idea is to expose "hidden" datatypes.
 2015-02-23 22:27:30 -08:00
Leonardo de Moura
7adecaf494 fix(frontends/lean/structure_cmd): include context/section parameteres/variables that are used in explicit structure parameters 2015-02-23 15:28:43 -08:00