Sebastian Ullrich
cfbc449769
refactor(frontends/lean/structure_cmd): some more cleanup
2017-04-26 14:22:46 -07:00
Sebastian Ullrich
d968b9a1c8
fix(frontends/lean/structure_cmd): remove evil Pi overload that accidentally abstracted constants in structure decls
2017-04-26 14:22:36 -07:00
Leonardo de Moura
cabb4350d9
feat(library): instances are not reducible by default anymore
...
Motivation: see "Other goodies" section at
https://github.com/leanprover/lean/wiki/Refactoring-structures
We had to add a new transparency mode: Instances at type_context.
In this mode, instances and reducible definitions are considered
transparent.
The new mode is used in the defeq_canonizer, code generator,
and sizeof lemma generation at inductive_compiler.
We also use the new mode in the unfold tactics.
2017-04-26 14:10:11 -07:00
Leonardo de Moura
08e094139d
feat(library/init/meta): add by_contradiction and by_cases to tactic.interactive
2017-04-26 12:54:52 -07:00
Leonardo de Moura
bcf34f1b6f
fix(library/inductive_compiler/nested): do not crash if we fail to unfold sizeof
2017-04-26 12:54:52 -07:00
Sebastian Ullrich
0d02136a09
fix(frontends/lean/inductive_cmds): do not whnf pre-exprs
...
Fixes #1507
2017-04-25 17:47:29 -07:00
Sebastian Ullrich
dd1f3e5f8c
fix(frontends/lean/structure_cmd): reject internal field names
...
Fixes #1539
2017-04-25 17:47:08 -07:00
Johannes Hölzl
b27100ec5a
fix(library/init/meta/transfer): add check if target contains (universe) meta variables (see #1535 )
2017-04-25 17:46:48 -07:00
Leonardo de Moura
cdafd4b791
chore(library): cleanup proofs
2017-04-25 17:23:42 -07:00
Leonardo de Moura
e59fd2927a
feat(library): process explicit arguments before implicit
...
Moreover, we process the implicit arguments using at least the Semireducible
transparency mode. The idea is to make sure to reduce counterintuitive
behavior in rw and simp where the user believes a lemma is applicable
but it does not work because the implicit part fails to unify.
The modification above fixes the simplifier issues found by @kha when proving the
monadic laws.
This commit also improves constraints of the form
n =?= m
where n and m are big distinct numerals. The type_context fails quickly
for this kind of constraint even using transparency mode Semireducible.
We need this feature otherwise we timeout at
@eq char a b =?= @eq unsigned ?x ?y
Recall that
char := fin char_sz
unsigned := fin unsigned_sz
2017-04-25 17:16:06 -07:00
Leonardo de Moura
e51ff591f7
chore(library/type_context): disable all trace messages inside type class resolution if trace.class_instances is not set to true
2017-04-25 14:16:10 -07:00
Leonardo de Moura
d0dede53f5
chore(library/tactic): make sure "pattern" is the first argument of is_def_eq
2017-04-25 09:59:04 -07:00
Sebastian Ullrich
e9a6c544af
refactor(frontends/lean/{elaborator,structure_cmd}): compile structure inheritance to nested fields
2017-04-24 19:35:15 +02:00
Sebastian Ullrich
cdd3f7fd6e
fix(util/rb_tree): fix remove(rb_tree)
2017-04-24 19:31:56 +02:00
Sebastian Ullrich
b26d15b9e9
fix(frontends/lean/elaborator): error message
2017-04-24 19:31:15 +02:00
Mario Carneiro
7ef4428124
add new interactive tactics skip, ginduction, exacts
2017-04-23 11:48:33 -07:00
Mario Carneiro
5e8572b407
add set.Union and set.univ
2017-04-23 11:37:27 -07:00
Jared Roesch
4704b68035
chore(*): remove smt2 bindings from standard libary
2017-04-23 11:32:11 -07:00
Sebastian Ullrich
6ab0a008f9
feat(frontends/lean/{builtin_cmds,interactive}): complete namespace/section after end
2017-04-23 11:26:31 -07:00
Sebastian Ullrich
a54514fead
feat(frontends/lean/print_cmd): complete identifiers after #print
2017-04-23 11:26:31 -07:00
Sebastian Ullrich
5b17c3cbd9
fix(frontends/lean/interactive): fall back to elaborator info when not an interactive tactic
...
Fixes #1530
2017-04-23 11:26:31 -07:00
Sebastian Ullrich
39a2ada9e7
fix(emacs/lean-type): cache docs to remove eldoc flickering
2017-04-23 11:26:31 -07:00
Gabriel Ebner
c2068dae46
fix(frontends/lean/tactic_notation): show error for unsolved focused goals at the end
...
Fixes #1531 .
2017-04-23 11:23:08 -07:00
Gabriel Ebner
489b3304bd
fix(frontends/lean/parser): allow enabling profiler via set_option
2017-04-23 11:22:50 -07:00
Gabriel Ebner
9424e6fa24
refactor(frontends/lean/definition_cmds): make profiling threshold configurable
2017-04-23 11:22:41 -07:00
Gabriel Ebner
d1e8a83212
fix(library/vm/interaction_state): do not show empty lines if profiling data is missing
2017-04-23 11:22:33 -07:00
Joe Hendrix
17291b8a33
refactor(library/data/vector): allow tail to accept empty vector.
2017-04-23 11:22:09 -07:00
Leonardo de Moura
e7603df514
feat(library/init/algebra): add type classes for algebraic normalizer
2017-04-18 15:47:38 -07:00
Sebastian Ullrich
b3884d5f42
refactor(init/meta/interactive,frontends/lean/token_table): introduce generalizing keyword in Lean
2017-04-16 15:11:49 -07:00
Leonardo de Moura
0d97700c60
feat(library/compiler): add support for and.rec in the code generator
2017-04-16 13:31:37 -07:00
Leonardo de Moura
470f2bc547
feat(library/compiler, library/vm): remove additional irrelevant information
2017-04-16 12:46:14 -07:00
Leonardo de Moura
969472af4f
chore(doc): remove old todo list
2017-04-16 09:49:21 -07:00
Sebastian Ullrich
26ac6d31f2
fix(library/metavar_util): do not compress mvar assignments in tmp mode
2017-04-16 09:35:49 -07:00
Leonardo de Moura
f6556ecdcc
fix(library/init): missing has_sizeof instances for subtype, char and string
2017-04-15 23:31:14 -07:00
Leonardo de Moura
210b7c8fb7
fix(library/tactic): fixes #1513
...
Implement rename tactic in Lean using revert/intro
2017-04-15 11:34:24 -07:00
Leonardo de Moura
fe0b694a06
feat(library/type_context): do not cache whnf in tmp_mode if term contains metavariables
2017-04-13 18:15:34 -07:00
Leonardo de Moura
7cc68130b3
feat(library/type_context): remove assign regular uvars hack
2017-04-13 18:15:29 -07:00
Leonardo de Moura
e40dbffba9
chore(library): add auxiliary lemmas for hoare state monad experiment
2017-04-12 18:01:59 -07:00
Sebastian Ullrich
8ea2bc08cb
feat(init/meta/interactive): add generalizing parameter to induction
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
17204f9629
feat(library/vm/interaction_state): capture tactic profile data if enabled
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
4483e53de0
feat(init/util): tactic.trace-like trace_val function
...
Calling it `trace` and removing the old `trace` function does bad things with overloading
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
70a2c402ac
feat(init/meta/interactive): Isabelle-like case tactic
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
c8c8c27654
feat(init/meta): add has_to_format instances and prefer direct has_to_tactic_format implementations
2017-04-11 17:07:28 -07:00
Sebastian Ullrich
026c5ee509
fix(library/init/meta/expr,library/vm/vm_expr): fix macro args
2017-04-11 17:07:28 -07:00
Gabriel Ebner
66cd4c57cf
feat(library/system/io): alternative instance for io
2017-04-11 16:42:17 -07:00
Gabriel Ebner
cefc26d9cb
refactor(library/system/process): add exit status and working directory
2017-04-11 16:42:17 -07:00
Gabriel Ebner
acf75bd69b
fix(library/handle): handle double close
2017-04-11 16:42:17 -07:00
Gabriel Ebner
e2fa363423
feat(library/system/io,shell/lean): add --run switch
2017-04-11 16:41:30 -07:00
Gabriel Ebner
e1fae7b761
fix(library/module): correctly print kernel exceptions
2017-04-10 15:59:31 +02:00
Gabriel Ebner
01a7efc007
fix(library/module_mgr): do not crash on missing imports
...
Fixes #1506 .
2017-04-04 19:56:33 +02:00
