Leonardo de Moura
45c8cdc626
fix(kernel/default_converter): discard constraints when optimization fails
2015-05-07 15:02:29 -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
ac24f19210
fix(library/tactic/rewrite_tactic): use relaxed type checker when processing rewrite "proof step"
...
That is, the restricted type checker should only be used in the
matching/unification step.
fixes #583
2015-05-07 09:57:23 -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
16b7bc3922
fix(kernel/default_converter): broken optimization
...
we must also check the universe levels when applying the optimization for
constraints of the form:
f.{l_1 ... l_k} a_1 ... a_n =?= f.{l_1' ... l_k'} b_1 ... b_n
The optimization tries to avoid unfolding f if we can establish that
a_i is definitionally equal to b_i for each i in [1, n]
closes #581
2015-05-06 18:32:41 -07:00
Leonardo de Moura
e841852be4
feat(library/max_sharing): maximize sharing in universe level expressions
2015-05-06 14:26:12 -07:00
Leonardo de Moura
210cae7d6c
fix(library/tactic): we must unfold untrusted macros when type checking intermediate results
...
Example: before this commit, the file librata/data/list/perm.lean would
not type check if the option -t 0 (trust level zero) was provided.
Reason: the intermediate term contained a macro, and macros are not
allowed at trust level zero.
2015-05-06 14:23:58 -07:00
Leonardo de Moura
b5619c2109
fix(library/export): remove workaround from 'export' procedure
...
The workaround was needed due to a bug in the max_sharing procedure
2015-05-06 14:00:57 -07:00
Leonardo de Moura
2ca16a099b
fix(library/max_sharing): conflict with the kernel approximate caching
2015-05-06 13:57:36 -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
84deddcca9
feat(library/tactic/rewrite_tactic): apply 'reflexivity' tactic after 'rewrite' instead of hard coded solution
2015-05-05 20:23:49 -07:00
Leonardo de Moura
c7a20644c0
fix(library/tactic/rewrite_tactic): bug in rewrite tactic (HoTT mode)
...
closes #580
2015-05-05 19:25:15 -07:00
Leonardo de Moura
a4efefb6ff
feat(library/tactic/rewrite_tactic): display type error message when
...
rewrite tactic fails
2015-05-05 19:23:41 -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
c0c0490db3
feat(library/export): simplify format
2015-05-04 18:22:12 -07:00
Leonardo de Moura
701b0ae66f
feat(library): export environment in textual format
...
closes #577
2015-05-04 18:05:00 -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
3c8c75470f
fix(library/tactic/exact_tactic): do not report unassigned metavariables in the 'refine' tactic
2015-05-03 21:08:09 -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
326048df54
feat(library/tactic/inversion_tactic): clear variables that have been eliminated by cases tactic
...
see discussion at:
https://groups.google.com/forum/#!topic/lean-discuss/oyzgIqdMyNc
2015-05-02 19:33:59 -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
e1dc18f6b6
fix(library/tactic/inversion_tactic): check whether eliminator can only eliminate to Prop
...
fixes #571
2015-05-02 17:48:08 -07:00
Leonardo de Moura
e379034b95
feat(library/tactic): improve 'assumption' tactic
...
- It uses the unifier in "conservative" mode
- It only affects the current goal
closes #570
2015-05-02 17:33:54 -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
b39fe17dee
feat(library/tactic): add 'transitiviy', 'reflexivity' and 'symmetry' tactics
...
closes #500
2015-05-02 15:48: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
415ca2b93f
feat(library/tactic): add 'congruence' tactic
...
It is the f_equal described at issue #500 .
2015-05-02 12:58:46 -07:00
Leonardo de Moura
2054d67483
chore(library/tactic/rewrite_tactic): fix style
2015-05-01 19:49:48 -07:00
Leonardo de Moura
9dc0388022
fix(library/tactic/rewrite_tactic): bug when rewriting hypotheses
2015-05-01 19:45:23 -07:00
Leonardo de Moura
ac8ba6a3cf
feat(library/tactic): add 'subst' tactic
...
see issue #500
2015-05-01 19:31:24 -07:00
Leonardo de Moura
b0759f3986
fix(library/tactic/rewrite_tactic): bug when rewriting multiple hypotheses
2015-05-01 19:03:43 -07:00
Leonardo de Moura
de369a0a0a
feat(library/tactic/injection_tactic): improve 'injection' tactic
...
see issue #500
2015-05-01 15:49:56 -07:00
Leonardo de Moura
9ba8b284a1
fix(library/tactic/apply_tactic): add eapply, and fix issue #361
2015-05-01 15:08:00 -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
Leonardo de Moura
63eb155c7e
feat(library/tactic): add 'injection' tactic
...
see issue #500
2015-05-01 12:45:21 -07:00
Leonardo de Moura
7e9f574ef3
fix(library/tactic/apply_tactic): use internally 'apply' instead of 'fapply' as the default "apply" tactic
...
This changes improves the 'constructor' tactic
2015-04-30 21:58:35 -07:00
Leonardo de Moura
2d9c950144
feat(library/tactic/constructor_tactic): allow 'constructor' tactic without index
...
see issue #500
2015-04-30 21:15:07 -07:00
Leonardo de Moura
15e52b06df
fix(library/tactic/constructor_tactic): bug in constructor tactic
...
see example (constr_tac2.lean) in comment at issue #500
2015-04-30 20:18:24 -07:00
Leonardo de Moura
d18f9c7607
fix(library/tactic/constructor_tactic): use 1 (instead of 0) to reference the first constructor
...
see comment at issue #500
2015-04-30 20:08:00 -07:00
Leonardo de Moura
0b995c4fe3
fix(library/tactic/rewrite_tactic): relax reducibility constraints in some parts of the rewrite tactic
...
fixes #567
2015-04-30 18:22:58 -07:00
