Leonardo de Moura
8c50048d1b
chore(frontends/lean/pp): fix style
2014-12-01 17:15:30 -08:00
Leonardo de Moura
320971832d
feat(frontends/lean/pp): add hard-coded pretty printer for nat numerals
2014-12-01 16:07:55 -08:00
Leonardo de Moura
8dfd22e66c
feat(frontends/lean): add 'prelude' command, and init directory
2014-11-30 17:03:08 -08:00
Leonardo de Moura
2281fb30c8
refactor(library): use "symbolic" precedences in the standard library
2014-11-29 19:08:37 -08:00
Leonardo de Moura
2c0472252e
feat(frontends/lean): allow expressions to be used to define precedence, closes #335
2014-11-29 18:29:48 -08:00
Leonardo de Moura
2487e3b83d
fix(frontends/lean/parser): user provided numeral notation should have precedence over the default based on 'num'
2014-11-29 17:29:03 -08:00
Leonardo de Moura
bc65aeb5e1
fix(frontends/lean/calc): add expected type for single-step calc expressions, fixes #357
...
This is not an issue for calc expressions containing multiple steps,
since the transitivity step will "force" the expected type for the proofs.
2014-11-29 15:35:09 -08:00
Leonardo de Moura
a97d7ffed7
feat(frontends/lean/builtin_cmds): display 'print' command output as flycheck information
2014-11-29 13:31:42 -08:00
Leonardo de Moura
366bf70ccd
fix(frontends/lean/elaborator): do not display flycheck related messages when --flycheck is not on
2014-11-28 21:20:25 -08:00
Leonardo de Moura
8b804f1d22
feat(frontends/lean): add option 'elaborator.flycheck_goals'
2014-11-28 16:34:02 -08:00
Leonardo de Moura
9516cd9ee3
feat(library/tactic): 'exact' tactic report unsolved placeholders in nested expression
...
Actually, the elaborator is the one reporting the unassigned
placeholders. The 'exact' tactic just makes the request.
To implement this feature we had to extend the elaboration interface
expected by the tactic framework.
2014-11-28 14:59:35 -08:00
Leonardo de Moura
4ec2101b06
feat(frontends/lean): add option 'pp.purify_locals'
2014-11-28 14:49:00 -08:00
Leonardo de Moura
db9fd53b80
fix(library/tactic): pretty printer for proof states
2014-11-27 09:43:58 -08:00
Leonardo de Moura
ffdeb0edc4
fix(frontends/lean/elaborator): unsolved metavariables, fix #329
2014-11-26 11:56:39 -08:00
Leonardo de Moura
24a15b6c46
fix(frontends/lean): disable class-instance resolution when executing find_decl, fixes #343
2014-11-24 21:33:52 -08:00
Leonardo de Moura
a005c8f4d0
feat(frontends/lean): display eval/check/find_decl results using flycheck
2014-11-24 08:35:49 -08:00
Leonardo de Moura
d81a6259e8
feat(frontends/lean/find_cmd): add options for controlling find_decl
2014-11-24 00:16:10 -08:00
Leonardo de Moura
f1e915a188
feat(frontends/lean): add 'find_decl' command
2014-11-23 23:00:59 -08:00
Leonardo de Moura
8c8bf41e39
feat(frontends/lean/server): do not unfold definitions in FINDG
2014-11-23 19:03:39 -08:00
Leonardo de Moura
44a2ef8f6f
fix(frontends/lean/parser_config): binder(s) rbp was not being saved in .olean file
2014-11-23 17:49:14 -08:00
Leonardo de Moura
64686c1278
feat(frontends/lean): allow user to associate precedence to binders, closes #323
2014-11-23 17:30:46 -08:00
Leonardo de Moura
cf3b0e1087
feat(frontends/lean/placeholder_elaborator): apply substitution before collecting local instances, closes #333
2014-11-23 17:30:46 -08:00
Leonardo de Moura
5d5fd2da50
fix(frontends/lean): tactic + section variables, fixes #332
2014-11-21 10:07:16 -08:00
Leonardo de Moura
28c63e685b
feat(frontends/lean): add '[local]' notation, closes #322
2014-11-16 21:15:04 -08:00
Leonardo de Moura
ea640257bf
feat(frontends/lean/structure_cmd): generate no_confusion for structures too
2014-11-15 16:00:09 -08:00
Leonardo de Moura
7685516d1e
feat(frontends/lean): better default for atomic notation
2014-11-14 16:25:13 -08:00
Leonardo de Moura
488f989c46
fix(frontends/lean/inductive_cmd): generate error for inductive datatype declarations that will produce an eliminator that can only eliminate to Prop
2014-11-14 13:57:42 -08:00
Leonardo de Moura
58525905d0
fix(frontends/lean/notation_cmd): bugs in 'reserve notation' command
2014-11-13 22:05:55 -08:00
Leonardo de Moura
6bc89f0916
feat(library/definitional): define ibelow and below
...
These are helper definitions for brec_on and binduction_on
2014-11-12 16:38:46 -08:00
Leonardo de Moura
a3066e3eaa
fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator
2014-11-12 13:10:19 -08:00
Leonardo de Moura
5312afa7ec
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes
...
The new test contains examples that required explicit levels.
2014-11-12 10:52:32 -08:00
Leonardo de Moura
e2bfe6ee36
refactor(library/definitional/no_confusion): cleanup API
2014-11-11 16:12:44 -08:00
Leonardo de Moura
f6889951c6
fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion
2014-11-11 15:14:08 -08:00
Leonardo de Moura
902a551048
feat(definitional/brec_on): add 'mk_below' skeleton
2014-11-11 14:55:21 -08:00
Leonardo de Moura
1079d6b320
refactor(library/definitional): combine auxiliary functions used by definitional package in a single module
2014-11-11 13:46:36 -08:00
Leonardo de Moura
50973bb4f3
feat(frontends/lean): default 'eval' command ignores opaque/irreducible annotations
...
To retrieve the previous behavior, we should use [strict] modifier
2014-11-10 12:46:04 -08:00
Leonardo de Moura
95554a527c
feat(frontends/lean/placeholder_elaborator): display instance trace header once per class-instance resolution problem
2014-11-09 15:00:13 -08:00
Leonardo de Moura
fa26c2301c
fix(frontends/lean): fix pretty-printing spacing problem
2014-11-09 14:49:43 -08:00
Leonardo de Moura
3aac26d658
fix(frontends/lean): tactic + variables bug, fixes #315
2014-11-09 14:43:22 -08:00
Leonardo de Moura
eff3c6b774
feat(frontends/lean): add variation of the foldl/foldr notation where initial element is suppressed, closes #314
...
See tests/lean/fold.lean for examples
2014-11-09 14:08:33 -08:00
Leonardo de Moura
ce889ddf60
feat(frontends/lean/scanner): disallow hierarchical names such as 'x.1'
2014-11-09 12:55:13 -08:00
Leonardo de Moura
df5a17cdce
feat(frontends/lean/placeholder_elaborator): include type in class-instance resolution trace
2014-11-09 12:06:16 -08:00
Leonardo de Moura
1d9a0a6265
feat(frontends/lean/placeholder_elaborator): add option 'elaborator.instance_max_depth'
2014-11-09 11:59:44 -08:00
Leonardo de Moura
9b9ae128d5
feat(frontends/lean): include file-name and line/col numbers when displaying class-instance resolution trace
2014-11-09 11:47:01 -08:00
Leonardo de Moura
6362610411
fix(frontends/lean): include position information
2014-11-09 11:43:44 -08:00
Leonardo de Moura
76fb6893e1
feat(frontends/lean): add elaborator.trace_instances option
...
When on this option allows us to visualize "class-instance resolution"
2014-11-09 11:24:19 -08:00
Leonardo de Moura
0b8c44a94a
feat(frontends/lean): add option pp.purify_metavars
...
It is true by default. If the user sets it to false, then
the internal metavariable names are used in the pretty printer
2014-11-09 11:04:22 -08:00
Leonardo de Moura
e8bc0f8249
feat(library/defitional): add no_confusion construction for inductive datatypes that are not propositions
2014-11-08 18:56:52 -08:00
Leonardo de Moura
b5da143fc0
feat(library/defitional): add no_confusion_type construction for inductive datatypes that are not propositions
2014-11-08 15:20:19 -08:00
Leonardo de Moura
c7992f2cac
feat(frontends/lean): add [whnf] modifier to eval command
2014-11-08 10:19:29 -08:00
Leonardo de Moura
b5e0ded163
feat(frontends/lean): max precedence used by Lean is not max_uint anymore
...
The motivation is to allow users to define notation with higher
precedence than function application.
2014-11-07 07:57:11 -08:00
Leonardo de Moura
85d0521d48
feat(frontends/lean): add '[parsing-only]' modifier to notation declarations, closes #305
2014-11-06 21:34:05 -08:00
Leonardo de Moura
be52d950f0
fix(frontends/lean): improve error message, addresses issue #299
2014-11-06 12:19:40 -08:00
Leonardo de Moura
8723f5b613
fix(frontends/lean/inductive_cmd): inductive datatype elaborator was 'fixing' parameter mismatches.
...
Given a datatype C with parameters As, if the declaration contained
(C Bs), the elaborator would silently replace it with (C As).
This bug would confuse users and make them believe they define something
different.
2014-11-05 23:12:00 -08:00
Leonardo de Moura
b3ad8c704a
feat(frontends/lean/structure_cmd): allow inheritance from two identical structures, closes #296
2014-11-05 15:01:05 -08:00
Leonardo de Moura
4650791108
feat(frontends/lean): add 'print fields' command
2014-11-05 14:06:54 -08:00
Leonardo de Moura
677e0aeef6
fix(frontends/lean/structure_cmd): accept ': Type' when universe levels are not specified
2014-11-05 12:02:52 -08:00
Leonardo de Moura
d6dc624ca8
fix(frontends/lean/structure_cmd): error parsing structure without parameters followed by ': Type'
2014-11-05 12:02:52 -08:00
Leonardo de Moura
defc2478b5
feat(frontends/lean): add 'record' as an alias for 'structure' command
2014-11-05 12:02:52 -08:00
Leonardo de Moura
5b87d060cf
fix(frontends/lean/structure_cmd): universe level validation
2014-11-04 22:19:23 -08:00
Leonardo de Moura
6944c7d902
fix(frontends/lean/placeholder_elaborator): local context must be adjusted when performing class-instance resolution modulo Pi-abstraction, fixes #293
2014-11-04 18:41:27 -08:00
Leonardo de Moura
b5ad0fb504
refactor(frontends/lean/local_context): add 'const' modifier
2014-11-04 18:37:31 -08:00
Leonardo de Moura
3bfe5b0b7e
fix(frontends/lean): type information for "atomic" notation declaration, fixes #292
2014-11-04 18:01:20 -08:00
Leonardo de Moura
fa405d7884
refactor(frontends/lean): combine info annotations in a single module
2014-11-04 18:01:20 -08:00
Leonardo de Moura
60eac0195d
feat(frontends/lean/structure_cmd): generate projection over constructor theorems for structures
2014-11-04 09:10:25 -08:00
Leonardo de Moura
d58c3e498d
feat(frontends/lean/builtin_cmds): add 'print prefix' command
2014-11-04 08:40:32 -08:00
Leonardo de Moura
3454e70017
fix(frontends/lean/inductive_cmd): bug in expression position propagation, fixes #289
...
Fix incorrect line/column number information in error messages produced
during inductive datatype elaboration.
2014-11-04 07:44:47 -08:00
Leonardo de Moura
b6722a5d33
feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures
...
When it is used coercions/instances to parent structure are to registered
2014-11-03 23:16:49 -08:00
Leonardo de Moura
b24165dc7b
feat(frontends/lean/structure_cmd): remove 'cases_on' for structures since it may confuse users, add 'destruct' as alternative name for 'rec_on'
2014-11-03 23:06:33 -08:00
Leonardo de Moura
7897e21a14
feat(frontends/lean/structure_cmd): allow fields to be suppresed, but constructor to be provided
2014-11-03 22:55:51 -08:00
Leonardo de Moura
08b4ce2db9
feat(frontends/lean/structure_cmd): use 'mk' as constructor name when it is not provided
2014-11-03 22:40:08 -08:00
Leonardo de Moura
8f3139231b
feat(frontends/lean/structure_cmd): allow structure declarations that contains only a header
2014-11-03 22:17:43 -08:00
Leonardo de Moura
91749d2364
fix(frontends/lean/structure_cmd): modify coercion generation
...
The previous coercion was more efficient, but the computation was
getting stuck when processing algebraic structures
2014-11-03 19:37:11 -08:00
Leonardo de Moura
c306bfa83c
feat(frontends/lean/structure_cmd): add 'eta' theorem for structures
2014-11-03 18:33:44 -08:00
Leonardo de Moura
186d910d0b
feat(frontends/lean/structure_cmd): mark coercion to parents as coercions and instances (when both structures as classes)
2014-11-03 17:55:59 -08:00
Leonardo de Moura
9531203d9d
feat(frontends/lean/structure_cmd): mark structure as 'class' when [class] modifier is used
2014-11-03 17:47:08 -08:00
Leonardo de Moura
b112f3c582
feat(frontends/lean/structure_cmd): add coercions to parent structures
2014-11-03 17:39:52 -08:00
Leonardo de Moura
922e66c42f
fix(frontends/lean/decl_cmds): do not save 'examples' in .ilean file
2014-11-03 16:13:46 -08:00
Leonardo de Moura
7afa69577e
feat(frontends/lean/structure_cmd): add aliases for structure decls
2014-11-03 15:50:41 -08:00
Leonardo de Moura
efe1105eb9
fix(frontends/lean): alias generation for composite names was not working
...
This is an issue for declarations that generate composite names such as
the inductive datatype packacke.
The commit also fix a bug in the generate of aliases for recursors
2014-11-03 15:43:58 -08:00
Leonardo de Moura
594e3ea8fc
fix(frontends/lean/structure_cmd): 'rec' must be marked as protected
2014-11-03 14:50:12 -08:00
Leonardo de Moura
5872c93eaf
feat(frontends/lean/structure_cmd): add structure_cmd core
2014-11-03 14:14:40 -08:00
Leonardo de Moura
a2e75159c8
fix(frontends/lean): process choice-exprs at check_constant_next
2014-11-02 19:42:30 -08:00
Leonardo de Moura
df008dc3c3
feat(frontends/lean/inductive_cmd): create a namespace for each declared datatype
2014-11-01 19:15:46 -07:00
Leonardo de Moura
ea55ec4090
feat(frontends/lean/decl_cmds): remove useless name from 'example' commad
2014-11-01 16:12:23 -07:00
Leonardo de Moura
1e6f7cdbb4
chore(frontends/lean/decl_cmds): add 'example' command
...
It is like a theorem, but it is discarded after checking
2014-11-01 11:37:39 -07:00
Leonardo de Moura
b1c2efecbb
chore(frontends/lean/decl_cmds): add missing static
2014-11-01 11:18:10 -07:00
Leonardo de Moura
94cf10284a
fix(frontends/lean/calc_proof_elaborator): bug when inserting symmetry proofs for heq, fixes #286
...
The problem was that heq type is
Pi {A : Type} (a : A) {B : Type} (b : B), Prop
The calc_proof_elaborator was assuming that (a : A) (b : B) were the
last two arguments in any relation supported by calc.
The fix is to remove this assumption.
2014-11-01 07:30:04 -07:00
Leonardo de Moura
2688ca38bf
feat(frontends/lean/inductive_cmd): notation for enumeration types
2014-10-31 19:01:32 -07:00
Leonardo de Moura
57b19b787b
feat(frontends/lean/calc_proof_elaborator): when 'elaborator.calc_assistant' is on, generate same info that is generated if !
was used
2014-10-31 09:49:45 -07:00
Leonardo de Moura
dc7ab17d2a
feat(frontends/lean/calc_proof_elaborator): add 'elaborator.calc_assistant' option
2014-10-31 09:49:45 -07:00
Leonardo de Moura
d7beabe91c
fix(frontends/lean/calc_proof_elaborator): improve calc proof assistant
2014-10-31 09:49:45 -07:00
Leonardo de Moura
8a4d4409cd
feat(frontends/lean/calc_proof_elaborator): add '{...⁻¹}' if needed in calc proofs, closes #268
...
This commit also simplifies library/data/nat/basic.lean
2014-10-31 01:02:49 -07:00
Leonardo de Moura
17df85f592
feat(frontends/lean/calc_proof_elaborator): add '{...}' if needed in calc proof steps
...
This is part of #268
2014-10-31 00:55:19 -07:00
Leonardo de Moura
42dba5cc98
feat(frontends/lean/calc): expose get_calc_subst_info and get_calc_refl_info APIs
2014-10-30 23:56:38 -07:00
Leonardo de Moura
591e566472
feat(frontends/lean): try to inject symmetry (if needed) in calc proofs, add calc_symm command for configuring the symmetry theorem for a given operator
...
This is part of #268
2014-10-30 23:24:09 -07:00
Leonardo de Moura
c5a62f8abb
feat(frontends/lean): insert !
in calculational proofs when needed
...
This is part of #268
2014-10-30 22:22:04 -07:00
Leonardo de Moura
407e35692b
feat(frontends/lean/calc): wrap calc proofs with 'proof-qed' annotation to identify places where proof influences what is being proved
...
Later, we will add a custom annotation and elaborator for calc proofs.
This is the first step for issue #268 .
Remark: we don't wrap the proof if it is of the form
- `by tactic`
- `begin tactic-seq end`
- `{ expr }`
2014-10-30 18:33:47 -07:00
Leonardo de Moura
e79c7d9852
feat(frontends/lean): make set_option
affect fingerprints
2014-10-30 14:45:35 -07:00
Leonardo de Moura
498b2f681e
feat(frontends/lean/placeholder_elaborator): better error message for ambiguous class-instance resolution
2014-10-30 14:44:58 -07:00
Leonardo de Moura
79f73c44dc
feat(frontends/lean/placeholder_elaborator): add 'elaborator.unique_class_instances' flag, closes #265
...
By default, it is false.
When it is true, class instance resolution generates an error if there
is more than one solution.
2014-10-30 14:21:24 -07:00
Leonardo de Moura
64c3ba7b74
feat(frontends/lean): display metavariable application arguments in check command
...
The idea is to "fix" counter-intuitive output like the ones were
produced in the tests check.lean and check2.lean
2014-10-30 13:28:25 -07:00
Leonardo de Moura
dcd7e53fa7
feat(frontends/lean/builtin_cmds): remove workaround for getting nice metavariable names in the check command
...
We don't need it anymore after previous commit 2a16050
2014-10-30 13:12:45 -07:00
Leonardo de Moura
2a160508c3
feat(frontends/lean): lean --server
should display meta-variables using the approach used in check command, closes #280
2014-10-30 12:45:41 -07:00
Leonardo de Moura
a1ea087f8e
fix(frontends/lean/info_manager): std::set insert is a noop if set already contains an equivalent element
2014-10-30 10:35:45 -07:00
Leonardo de Moura
6107da05db
fix(frontends/lean): universe variable is treated as parameter inside section, fixes #283
2014-10-29 19:47:14 -07:00
Leonardo de Moura
8e9f97e95e
fix(frontends/lean): do not save identifier info
2014-10-29 17:38:59 -07:00
Leonardo de Moura
c1653a9fb4
feat(frontends/lean): only valid proof states should be displayed, closes #275
2014-10-29 17:29:40 -07:00
Leonardo de Moura
a98b12f067
fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276
2014-10-29 16:51:06 -07:00
Leonardo de Moura
1c9992800f
fix(frontends/lean/info_manager): suppress useless tactic type information, closes #277
2014-10-29 16:51:06 -07:00
Leonardo de Moura
fe4ea48381
feat(library/definitional/projection): add projection generator, closes #257
2014-10-29 13:13:05 -07:00
Leonardo de Moura
0c185fc4ab
fix(library/tactic): add relax_main_opaque flag to proof_state objects, closes #274
2014-10-29 08:57:34 -07:00
Leonardo de Moura
a2ef835809
fix(frontends/lean): squiggle position for unary begin-end block
2014-10-28 23:26:24 -07:00
Leonardo de Moura
83e4c0fcec
feat(frontends/lean): hide tactic "types"
...
it is not very useful to display the type of tactics (e.g., apply,
intros, ...)
2014-10-28 22:38:10 -07:00
Leonardo de Moura
eeb6c72508
feat(frontends/lean): modify begin-end
semantics, closes #258
2014-10-28 22:15:38 -07:00
Leonardo de Moura
1c2bbcfebc
feat(frontends/lean/info_manager): add separator --
when displaying PROOF_STATE info
...
This feature was implemented to address issue #259
2014-10-28 16:39:21 -07:00
Leonardo de Moura
60f32fa709
fix(frontends/lean): begin-end
automatic tactic notation bug, fixes #262
2014-10-27 17:12:25 -07:00
Leonardo de Moura
7516fcad97
feat(kernel/type_checker): add is_stuck
method, and improve ensure_pi method, closes #261
2014-10-27 13:16:50 -07:00
Leonardo de Moura
2e5ad274a5
fix(frontends/lean/elaborator): remove invalid assertions
...
These assertions became invalid when we changed the behavior of undef
indentifiers at
8e6de93394
2014-10-27 10:31:09 -07:00
Leonardo de Moura
ee5a982c01
feat(shell/lean): add '--server-trace' flag, closes #264
2014-10-27 10:26:29 -07:00
Leonardo de Moura
d66e5a6c41
fix(frontends/lean/builtin_cmds): bug (name clashing) in 'check' command new meta-variable naming
2014-10-26 19:19:45 -07:00
Leonardo de Moura
81dc201bab
fix(frontends/lean/elaborator): nested begin-end bug
2014-10-26 18:23:30 -07:00
Leonardo de Moura
a544d32fcf
fix(frontends/lean/elaborator): missing information when displaying unsolved placeholders
2014-10-26 16:11:58 -07:00
Leonardo de Moura
cc6a96e8ba
fix(frontends/lean): improve begin-end construct
2014-10-26 15:47:29 -07:00
Leonardo de Moura
aed9a88b38
fix(frontends/lean/parser): save identifier info for undef local
2014-10-26 10:19:44 -07:00
Leonardo de Moura
8e6de93394
fix(frontends/lean/parser): add two kinds of no_undef_id behavior: to (global) constant; to local constant
2014-10-26 09:47:11 -07:00
Leonardo de Moura
707584376a
fix(frontends/lean/inductive_cmd): include 'induction_on', 'cases_on', and 'rec_on' into .ilean index file
2014-10-25 17:56:22 -07:00
Leonardo de Moura
c7f6a6b94e
feat(library/definitional/cases_on): automatically add 'cases_on'
2014-10-25 17:22:02 -07:00
Leonardo de Moura
cdcde661ef
feat(library/definitional/induction_on): automatically add 'induction_on'
2014-10-25 13:37:04 -07:00
Leonardo de Moura
a7a06ab0f8
feat(library/definitional/rec_on): automatically generate rec_on function for inductive datatypes
2014-10-25 13:08:59 -07:00
Leonardo de Moura
2bc034da2c
feat(kernel/inductive): expose 'get_elim_name' API
2014-10-25 10:47:12 -07:00
Leonardo de Moura
5830da9e2d
fix(frontends/lean/tokens): typo
2014-10-24 14:44:59 -07:00
Leonardo de Moura
7a033ac07e
feat(frontends/lean): add 'print axioms' command, close #251
2014-10-24 14:35:03 -07:00
Leonardo de Moura
db25f933b0
feat(frontends/lean): use nice names for meta-variables when executing check c
and c
is a constant
2014-10-24 08:23:26 -07:00
Leonardo de Moura
f027acb5cb
fix(frontends/lean): missing type info in expressions nested in tactics
2014-10-23 18:31:05 -07:00
Leonardo de Moura
a6571c3273
feat(frontends/lean): add 'print definition' command
2014-10-23 14:54:15 -07:00
Leonardo de Moura
22ae42d3af
fix(frontends/lean/info_manager): use fresh formatter displaying each info object
...
The formatter may cache results.
2014-10-23 14:29:17 -07:00
Leonardo de Moura
20ab59c740
fix(frontends/lean/pp): avoid unnecessary parentheses when pretty printing delimited notation
2014-10-23 14:14:08 -07:00
Leonardo de Moura
212ae0b61c
feat(frontends/lean): automatically add 'info' tactic in begin-end blocks
...
Actually, the tactic is only added when Lean is in collect-info mode.
2014-10-23 13:30:04 -07:00
Leonardo de Moura
e750c9b67a
feat(frontends/lean): add 'info' tactic for producing PROOF_STATE info for emacs mode
2014-10-23 13:18:30 -07:00
Leonardo de Moura
cadc9b3ff3
feat(frontends/lean/info_manager): add proof_state info
2014-10-23 10:40:07 -07:00
Leonardo de Moura
38a9aa2a98
feat(frontends/lean): automatically open 'tactic' namespace (if it is not already open) in 'by' and 'begin-end' expressions
2014-10-23 10:26:19 -07:00
Leonardo de Moura
2c330e704e
fix(frontends/lean/elaborator): error localization for 'expr_to_tactic' failures
2014-10-23 10:26:19 -07:00
Leonardo de Moura
f3fdc70400
refactor(library/tactic): add auxiliary module 'library/tactic/elaborate'
2014-10-23 10:26:11 -07:00
Leonardo de Moura
7c62446023
refactor(frontends/lean): remove dead code
2014-10-22 17:39:06 -07:00
Leonardo de Moura
eb2b59ce4f
refactor(frontends/lean): remove unnecessary files
2014-10-22 17:33:16 -07:00
Leonardo de Moura
e95c7c5f70
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement 'intro/intros' tactic
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-10-22 17:29:50 -07:00
Leonardo de Moura
9a316092d1
refactor(library/tactic/rename_tactic): use new 'tactic.expr' to implement rename tactic
2014-10-22 17:29:50 -07:00
Leonardo de Moura
5e15ac0c92
feat(library/tactic): add new approach for embedding non-elaborated expressions into tactics
2014-10-22 17:29:50 -07:00
Leonardo de Moura
7c617955d0
refactor(library/tactic): move 'exact' tactic to separate module
2014-10-22 17:29:44 -07:00