Leonardo de Moura
|
f64784378a
|
fix(frontends/lean/pp): make pp_have more robust
We should not assume the argument of a have_annotation is a lambda.
|
2015-06-10 16:26:20 -07:00 |
|
Leonardo de Moura
|
ca43f6e62e
|
refactor(frontends/lean): add postprocess procedure and cleanup
|
2015-06-10 15:19:35 -07:00 |
|
Leonardo de Moura
|
4b91cfccff
|
feat(frontends/lean/builtin_exprs): make notation ( e : T ) builtin
In the previous approach, the following (definitionally equal) term was being generated
(fun (A : Type) (a : A), a) T e
|
2015-06-10 14:52:59 -07:00 |
|
Leonardo de Moura
|
f7dd85a935
|
chore(*): fix 'breif' typos
|
2015-06-08 16:54:55 -07:00 |
|
Leonardo de Moura
|
d0d3f9bb41
|
refactor(kernel,library,frontends/lean): add helper functions, and cleanup collect_locals
|
2015-06-05 17:29:36 -07:00 |
|
Leonardo de Moura
|
c76d92284f
|
feat(library/pp_options): add 'pp.all' option
|
2015-06-05 08:41:46 -07:00 |
|
Leonardo de Moura
|
134740182d
|
fix(frontends/lean): fixes #652
|
2015-06-03 21:53:51 -07:00 |
|
Leonardo de Moura
|
0fbc944cdd
|
feat(frontends/lean): add '[rewrite]' attribute
|
2015-06-01 17:58:24 -07:00 |
|
Leonardo de Moura
|
d547698a56
|
refactor(library,library/tactic): move class_instance_synth to library
This module will be needed by the simplifier
|
2015-06-01 16:30:40 -07:00 |
|
Leonardo de Moura
|
b6fde68012
|
feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples"
|
2015-06-01 15:35:28 -07:00 |
|
Leonardo de Moura
|
55608c9b9f
|
fix(frontends/lean/pp): bug in pp arrow
|
2015-05-31 17:21:37 -07:00 |
|
Leonardo de Moura
|
ca110012d8
|
feat(library/tactic): automate "generalize-intro-induction/cases" idiom
closes #645
|
2015-05-30 21:57:28 -07:00 |
|
Leonardo de Moura
|
e5a82ef516
|
feat(frontends/lean): add option for disabling "coercion lifting"
|
2015-05-30 17:07:42 -07:00 |
|
Leonardo de Moura
|
6f6848968d
|
feat(frontends/lean/coercion_elaborator): "coercion lifting" for backtracking case
closes #252
|
2015-05-30 16:44:26 -07:00 |
|
Leonardo de Moura
|
ea9c810fca
|
feat(frontends/lean/coercion_elaborator): implement "coercion lifting"
closes #644
|
2015-05-30 14:45:14 -07:00 |
|
Leonardo de Moura
|
6d2f37857d
|
feat(frontends/lean/builtin_cmds): add 'print [reducible]', 'print [irreducible]' and 'print [quasireducible]' commands
|
2015-05-29 16:47:29 -07:00 |
|
Leonardo de Moura
|
7a0e198147
|
feat(kernel,frontends/lean/builtin_cmds): allow kernel extensions to report their builtin constants
|
2015-05-29 16:28:16 -07:00 |
|
Leonardo de Moura
|
f48cdccd20
|
fix(frontends/lean/pp): abbreviation with parameters
closes #639
|
2015-05-29 15:13:31 -07:00 |
|
Leonardo de Moura
|
a071012346
|
fix(frontends/lean/pp,library/head_map): handle 'as_atomic' annotation
This commit fixes local notation that contains parameters
see issue #639
|
2015-05-29 14:51:28 -07:00 |
|
Leonardo de Moura
|
e6099583ad
|
feat(frontends/lean/builtin_cmds): expand abbreviations in the 'check' command
see issue #639
|
2015-05-29 14:51:07 -07:00 |
|
Leonardo de Moura
|
3b7b268e40
|
fix(frontends/lean/pp): fixes #634
trying again...
|
2015-05-29 14:07:38 -07:00 |
|
Leonardo de Moura
|
7f12401ea7
|
fix(frontends/lean/elaborator): save type information for 'obtain' declarations
|
2015-05-29 10:16:12 -07:00 |
|
Leonardo de Moura
|
7342f342a9
|
fix(frontends/lean/pp): fixes #634
|
2015-05-28 19:43:49 -07:00 |
|
Leonardo de Moura
|
85409a59d3
|
feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants
closes #511
|
2015-05-27 16:32:43 -07:00 |
|
Leonardo de Moura
|
7d73f4f091
|
refactor(library,frontends/lean): simplify the creation of custom normalizers
|
2015-05-27 15:33:20 -07:00 |
|
Leonardo de Moura
|
47e5633498
|
feat(frontends/lean/calc_proof_elaborator): avoid unnecessary unfolding in the calc tactic
|
2015-05-27 12:07:39 -07:00 |
|
Leonardo de Moura
|
ea43f3ea80
|
fix(frontends/lean/builtin_cmds): fixes #630
|
2015-05-26 22:19:42 -07:00 |
|
Leonardo de Moura
|
4d1b711247
|
feat(frontends/lean/elaborator): better error localization when running out of stack space and/or memory in begin-end tactic mode.
|
2015-05-26 20:09:15 -07:00 |
|
Leonardo de Moura
|
0502f46f9b
|
fix(frontends/lean/scanner): another bug related to issue #626
|
2015-05-26 13:39:42 -07:00 |
|
Leonardo de Moura
|
25e41b9b09
|
fix(frontends/lean/scanner): fixes #626
|
2015-05-26 11:33:38 -07:00 |
|
Leonardo de Moura
|
ab58e538a4
|
feat(frontends/lean/elaborator): hide auxiliary 'match' hypothesis during elaboration
|
2015-05-25 15:24:56 -07:00 |
|
Leonardo de Moura
|
24b35eefe6
|
chore(frontends/lean/elaborator): add assertion for sanity checking
|
2015-05-25 14:04:27 -07:00 |
|
Leonardo de Moura
|
b83b0c0017
|
fix(library/tactic/induction_tactic): fixes #619
|
2015-05-21 18:22:07 -07:00 |
|
Leonardo de Moura
|
f830bf54c2
|
refactor(*): clarify name_generator ownership
|
2015-05-21 14:32:36 -07:00 |
|
Leonardo de Moura
|
c2faa0fe98
|
refactor(library): rename equivalence_manager to relation_manager
|
2015-05-21 12:25:02 -07:00 |
|
Leonardo de Moura
|
89581cead7
|
fix(frontends/lean/parser): fixes #616
|
2015-05-20 23:33:41 -07:00 |
|
Leonardo de Moura
|
2d22bb8ea2
|
feat(frontends/lean/builtin_cmds): do not unfold proofs in the eval command
In the future, we should probably add an option for unfolding proofs.
|
2015-05-20 19:14:57 -07:00 |
|
Leonardo de Moura
|
d5da659be7
|
feat(frontends/lean/elaborator): include overload information in error messages
|
2015-05-20 17:21:27 -07:00 |
|
Leonardo de Moura
|
76c3757db7
|
feat(frontends/lean/elaborator): use custom normalizers for detecting whether there are coercions from/to a given type
closes #547
|
2015-05-20 16:12:12 -07:00 |
|
Leonardo de Moura
|
608984cd4c
|
chore(frontends/lean/elaborator): cleanup ensure fun
|
2015-05-20 15:10:45 -07:00 |
|
Leonardo de Moura
|
af3f0088f4
|
feat(frontends/lean): add 'override' (notation) command
|
2015-05-20 11:42:16 -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
|
c133d26505
|
feat(frontends/lean/builtin_exprs): change how 'show' is processed in tactics
Unresolved placeholders were not being reported
|
2015-05-19 16:23:50 -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
|
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 |
|