Mario Carneiro
c5bb5cb1eb
fix(init/meta/interactive_base): declare |- notation
2017-08-17 11:34:00 +02:00
Leonardo de Moura
6315136279
fix(frontends/lean/definition_cmds): fixes #1790
2017-08-16 15:57:55 -07:00
Leonardo de Moura
19ee270c60
refactor(library): remove vector and bitvec from init
...
Reason: vector in in init folder was introducing an overload (`::`) for
all Lean users. The workaround (use `local infix ::`) was
counterintuitive.
We currently have no special support for bitvectors in the code
generator. Thus, there is no need to have vector and bitvec in the init
folder right now. Moreover, the new parser and elaborator (issue #1674 ) should
provide better ways of managing overloaded symbols.
2017-08-16 13:40:50 -07:00
Sebastian Ullrich
987e681323
chore(test/lean): add overlooked test
2017-08-15 12:45:14 +02:00
Sebastian Ullrich
579d4a459e
chore(init/meta/interactive): check simp lemmas for ambiguous overloads
...
Fixes #1786
2017-08-15 12:43:02 +02:00
Gabriel Ebner
b50597228b
chore(tests/lean/print_ax2): remove duplicate and broken test
2017-08-06 10:33:33 +02:00
Gabriel Ebner
e2717ec2c5
fix(library/compiler/inliner): inline auxiliary declarations
...
Fixes #1763 .
2017-08-06 10:24:26 +02:00
Gabriel Ebner
0c15724e8e
fix(library/tactic/simplify): handle universe polymorphic simplification rules
...
The issue was that instantiate_mvars(infer(m)) had a metavariable, while
infer(instantiate_mvars(m)) did not. Changing the call from assign to
is_def_eq also unifies the type, assigning the metavariable inside the
type.
2017-08-03 17:42:07 +01:00
Leonardo de Moura
b6c691cead
test(tests/lean/run/whnf_mvar): add test to check whether whnf instantiate mvars or not
...
@digama0 As I suspected, `whnf` already instantiates metavariables.
2017-08-03 11:29:22 +01:00
Gabriel Ebner
22011dcde4
chore(init/algebra/order): typo
...
Thanks to @fpvandoorn for proof-reading!
2017-08-02 15:41:51 +01:00
Leonardo de Moura
f39e42bf2d
fix(library/tactic/destruct_tactic): fixes #1766
2017-08-02 15:35:33 +01:00
Leonardo de Moura
fdaa26f2fd
feat(library/equations_compiler/wf_rec): fixes #1782
2017-08-02 15:12:04 +01:00
Gabriel Ebner
5922f71c50
feat(library/init/algebra/order): add default value for lt
2017-08-02 14:41:35 +01:00
Gabriel Ebner
ce509e621a
refactor(library/init/algebra): remove order_pair classes
2017-08-02 14:41:35 +01:00
Sebastian Ullrich
4f66673fc2
feat(init/meta/attribute,library/tactic/attribute): user_attribute apply handlers
2017-08-02 14:32:39 +01:00
Gabriel Ebner
becec82311
fix(frontends/lean/structure_cmd): simplify parser
2017-08-02 11:27:13 +01:00
Leonardo de Moura
39fa7625b8
feat(library/init/meta/interactive): add specialize tactic
...
closes #1779
2017-08-02 10:20:25 +01:00
Gabriel Ebner
c15f2979c6
fix(frontends/lean/util): allow docstrings after variables
2017-08-01 10:18:05 +01:00
Gabriel Ebner
89e1b196db
fix(library/compiler/preprocess): do not unfold noncomputable definitions
...
This happened in Johannes' real number formalization. We tried to
unfold a noncomputable definition even though it would have been erased
afterwards, and failed.
The check_computable check was introduced in order to fix the error
message in #1401 , the error message is still intelligible in that
example.
2017-08-01 08:37:18 +01:00
Gabriel Ebner
2804a0ea27
fix(util/name): escape empty name components using french quotes
2017-07-31 16:01:46 +01:00
Mario Carneiro
f369e34bd6
chore(library/standard): remove standard.lean (unused, and confusing given stdlib)
2017-07-28 16:47:53 +01:00
Mario Carneiro
ec82afb45a
fix(tests): fix tests
2017-07-28 16:47:02 +01:00
Leonardo de Moura
870ce5c0fe
fix(library/init/meta/constructor_tactic): fixes #1771
2017-07-28 09:45:51 +01:00
Sebastian Ullrich
c44ed73d56
fix(frontends/lean/scanner): minor lexical grammar fixup
2017-07-26 17:02:00 +02:00
Leonardo de Moura
58016bc037
chore(tests/lean): fix test suite
2017-07-26 14:10:02 +01:00
Leonardo de Moura
1ec65bed44
refactor(library/init): move bitvector to main repo
...
@digama0 I moved bitvec back to the main repo, and many nat lemmas.
I want these lemmas here for now. I will need some of them for future
decision procedures.
2017-07-26 13:35:38 +01:00
Mario Carneiro
4dc261393f
refactor(init/data/list): move out advanced list defs
2017-07-26 11:52:11 +01:00
Mario Carneiro
09f9cada65
chore(init/data/nat): rename add_one_eq_succ -> add_one
2017-07-26 11:52:10 +01:00
Mario Carneiro
cc81118892
refactor(init/data): move out some nat lemmas
2017-07-26 11:52:10 +01:00
Mario Carneiro
7d4fe55bff
fix(tests/lean/run/choice_anon_ctor): fix test
2017-07-26 11:52:10 +01:00
Mario Carneiro
74aeb250ec
refactor(*): move out stdlib
2017-07-26 11:52:10 +01:00
Gabriel Ebner
25aa847aba
fix(library/constructions/brec_on): make motive explicit in *.below
...
Otherwise you can't figure out the type from the pretty-printed output
`nat.below n`.
2017-07-23 09:38:44 +01:00
Leonardo de Moura
c7c8387bd8
chore(tests/lean/run/bin_tree): fix broken test
2017-07-21 05:05:42 -07:00
Leonardo de Moura
4faae27069
perf(frontends/lean): add notation #[...]
...
The new notation should be use to input long sequences.
Closes #1755
2017-07-21 04:20:48 -07:00
Mario Carneiro
94ecc3292f
fix(tests): fix tests
2017-07-21 02:10:48 -07:00
Mario Carneiro
97a01d25fd
fix(init/meta/tactic): skip solved goals in seq_focus and seq
...
and all/any_goals. This occurs when solving the first subgoal generated by `tac1; tac2` closes the second goal as well, before the second `tac2` invocation is run. Reported by @jldodds on gitter.
2017-07-21 02:10:48 -07:00
Sebastian Ullrich
7e619487f0
fix(frontends/lean/elaborator): suppress error messages containing synthetic sorrys
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
46c1a1a844
refactor(frontends/lean/elaborator,kernel/error_msgs): remove duplicate code
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
f8cfc4ea1b
feat(kernel/error_msgs,frontends/lean/elaborator): add more context to 'type/function expected' errors
2017-07-21 01:46:31 -07:00
Sebastian Ullrich
ae5bc52d97
fix(frontends/lean/elaborator): pass expected type through visit_function
2017-07-20 01:58:29 -07:00
Sebastian Ullrich
a1066525ca
feat(init/meta/interactive): auto-generalize inductive major premise args
...
Like Isabelle
2017-07-20 01:51:00 -07:00
Sebastian Ullrich
9ed72acabe
fix(frontends/lean/builtin_exprs): allow constant patterns in do notation
2017-07-20 01:51:00 -07:00
Sebastian Ullrich
7d39b3e948
refactor(init/meta/interactive): merge generalize and generalize2 and introduce nicer syntax
2017-07-20 01:51:00 -07:00
Gabriel Ebner
e94095cdf3
chore(library/tactic/cases_tactic): add a bit more information to error message
2017-07-18 09:07:09 +01:00
Sebastian Ullrich
9c2d42b269
fix(frontends/lean/parser): to_pattern_fn: replace invalid choice pattern with sorry
...
Fixes #1749
2017-07-17 14:59:07 +02:00
Gabriel Ebner
246d71f3ff
feat(library/equations_compiler): error recovery
2017-07-16 05:17:38 -07:00
Gabriel Ebner
9367e94900
fix(frontends/lean/pp): hide proof terms in non-proofs by default
...
This is mainly to reduce clutter. Proof term printing can still be
forced using the `pp.proofs` option.
2017-07-15 22:21:22 +01:00
Gabriel Ebner
37d9e03cc1
feat(frontends/lean/pp): show substituted expressions for delayed abstractions
...
@leodemoura I tried to look up the unique names in the local context,
but this pretty much always fails. AFAICT we never remember the local
context when pretty-printing expression texts.
2017-07-15 21:34:05 +01:00
Gabriel Ebner
9dcd95df2f
chore(tests/lean/anc1): fix tests
2017-07-15 21:13:33 +01:00
Gabriel Ebner
68ee9396c6
fix(frontends/lean/parser): support backtracking from empty expressions
...
Fixes #1745 .
2017-07-15 11:12:09 +01:00
