Leonardo de Moura
1f13bfa4f7
feat(library/tactic/inversion_tactic): add inversion::apply procedure
...
The new procedure is essentially a "customized" version of the
inversion (aka cases) tactic for the equations package
2015-01-01 19:33:14 -08:00
Soonho Kong
f370871574
fix(emacs/lean-syntax): highlight axioms
...
fix #382
2014-12-30 14:25:19 -05:00
Leonardo de Moura
0aa7e4a9f9
fix(frontends/lean/pp): option 'pp.private_names' should also affect private declarations defined in the current file
2014-12-28 14:22:36 -08:00
Leonardo de Moura
d082fb7402
fix(shell/lean): crash when trying to read file without extension
2014-12-28 14:22:36 -08:00
Jeremy Avigad
53f486835e
fix(library/data/nat/order): delete unused material at end of file
2014-12-26 16:57:10 -05:00
Jeremy Avigad
1eea75b6fc
fix(library/data/nat/div,tests/lean/run/ppbeta): make decidable for dvd transparent, name change in ppbeta
2014-12-26 16:44:43 -05:00
Jeremy Avigad
cecabbb401
refactor(library/data/int,library/algebra): make int an instnance of ordered ring, rename theorems
2014-12-26 16:25:05 -05:00
Jeremy Avigad
25394dddb7
refactor(library): change mul.left_id to mul_one, and similarly for mul.right_id, add.left_id, add.right_id
2014-12-23 21:14:36 -05:00
Jeremy Avigad
5bc6dd84cf
feat(library/data/nat): make nat an instance of comm_semiring
2014-12-23 21:14:35 -05:00
Jeremy Avigad
486bc321ff
refactor(library/data/nat): rename theorems
2014-12-23 21:14:35 -05:00
Jeremy Avigad
e587449a6d
refactor(library/data): remove folders with a single file
2014-12-23 21:14:35 -05:00
Leonardo de Moura
2be83fbff7
test(tests/lean): remove data.nat dependency
2014-12-23 17:42:56 -08:00
Jeremy Avigad
6ad091d7bf
refactor(library): clean up headers and markdown files
2014-12-22 15:33:42 -05:00
Jeremy Avigad
fe424add26
refactor(library/logic/axioms): rename theorems
2014-12-22 15:33:42 -05:00
Jeremy Avigad
0f0da64264
refactor(library/data/int): make int instance of integral domain
2014-12-22 15:33:42 -05:00
Jeremy Avigad
da7a403b6c
refactor(library/algebra/ring): make dvd a definition
2014-12-22 15:33:41 -05:00
Leonardo de Moura
264c88d332
test(tests/lean/hott): add tele_eq example using HoTT library
2014-12-22 09:43:16 -08:00
Leonardo de Moura
1d79cb9c07
fix(library/tactic/inversion_tactic): fix bug in 'cases' tactic for HoTT library
2014-12-22 09:40:15 -08:00
Leonardo de Moura
d2958044fd
feat(frontends/lean): add multiple_instances command
...
After this commit, Lean "cuts" the search after the first instance is
computed. To obtain the previous behavior, we must use the new command
multiple_instances <class-name>
closes #370
2014-12-21 17:28:44 -08:00
Leonardo de Moura
5efadb09cc
feat(library/tactic/inversion_tactic): improve 'cases' tactic for HoTT library
...
This commit adds support for hypotheses (h : C As idxs) where the indices idxs
are just local constants. Before this commit the indices idxs had to be hsets.
Now, they can be hsets or local constants.
The new tests demonstrate new examples that can be handled by the
improved tactic in the HoTT library
2014-12-21 15:19:25 -08:00
Leonardo de Moura
70f7ec3cf2
test(tests/lean/hott): add test for 'cases' tactic
2014-12-20 11:36:32 -08:00
Leonardo de Moura
0627ad2f56
feat(hott/init/nat): add basic facts about natural numbers
2014-12-20 11:32:27 -08:00
Leonardo de Moura
d75ef7a07a
feat(hott/init/types): add 'sum' notation
2014-12-20 11:32:27 -08:00
Leonardo de Moura
6843fe3a8b
refactor(hott/init): 'prod' and 'sum' notation should be infix right like 'and' and 'or'
2014-12-20 11:32:27 -08:00
Leonardo de Moura
677ec2a2fe
feat(library/tactic/inversion_tactic): adjust inversion tactic to HoTT lib
2014-12-20 11:32:27 -08:00
Leonardo de Moura
7a75325416
feat(kernel/abstract): add new abstract_local procedure
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-20 11:31:48 -08:00
Leonardo de Moura
2070ac849c
feat(library/util): add get_intro_rule_names
...
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-12-20 11:31:48 -08:00
Leonardo de Moura
d9d822baa7
feat(library/tactic/class_instance_synth): add mk_hset_instance procedure
2014-12-19 22:00:25 -08:00
Leonardo de Moura
8c63045492
feat(library/util): add more auxiliary procedures
2014-12-19 22:00:25 -08:00
Leonardo de Moura
187f4483e9
refactor(hott/init/util.hlean): modify definition to make it more convenient for definitional package
2014-12-19 22:00:25 -08:00
Leonardo de Moura
2e93e5d6a7
fix(hott/init): minimize number of universe parameters
2014-12-19 22:00:25 -08:00
Leonardo de Moura
d6f79423e9
feat(library/tactic/class_instance_synth): add mk_class_instance procedures
2014-12-19 20:09:09 -08:00
Leonardo de Moura
4421069e34
refactor(library/tactic): rename placeholder_elaborator to class_instance_synth
2014-12-19 19:57:38 -08:00
Leonardo de Moura
f93278eab8
fix(hott/init/hedberg): remove unnecessary import
2014-12-19 19:01:07 -08:00
Leonardo de Moura
2521dbb39e
refactor(hott): use same name convention for sigma in the HoTT and standard libraries
2014-12-19 18:46:06 -08:00
Leonardo de Moura
1e2fc54f2f
refactor(library/init/sigma): rename sigma.dpair->sigma.mk, sigma.dpr1->sigma.pr1, sigma.dpr2->sigma.pr2
2014-12-19 18:23:08 -08:00
Leonardo de Moura
9eea32b076
refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr
2014-12-19 18:07:13 -08:00
Leonardo de Moura
69191ef9b7
feat(hott/init/datatypes): add sum.intro_left and sum.intro_right aliases
2014-12-19 17:56:44 -08:00
Leonardo de Moura
ded869b7e0
refactor(frontends/lean): move placeholder_elaborator to library/tactic
2014-12-19 15:23:22 -08:00
Leonardo de Moura
a22dc773b7
refactor(frontends/lean): move some auxiliary procedures to library/tactic
2014-12-19 15:19:45 -08:00
Leonardo de Moura
07d7ea2f4e
refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean
2014-12-19 15:08:21 -08:00
Leonardo de Moura
69750c50c6
refactor(frontends/lean): move pp_options to library
2014-12-19 15:00:05 -08:00
Leonardo de Moura
caf0a4bf15
refactor(frontends/lean): move type_checker_ptr typedef to library
2014-12-19 14:40:15 -08:00
Leonardo de Moura
02de288a51
refactor(frontends/lean): move choice_iterator to library
2014-12-19 14:29:32 -08:00
Leonardo de Moura
3d2d5839a1
feat(hott/init): add auxiliary definition needed by definitional package
2014-12-19 14:22:03 -08:00
Leonardo de Moura
582c1f8458
feat(hott/init): add proof for Hedberg's theorem
2014-12-19 13:54:12 -08:00
Leonardo de Moura
9bd74689be
feat(library/util): add mk_refl
2014-12-19 13:54:12 -08:00
Leonardo de Moura
a97bef7df2
feat(library/util): add mk_heq
2014-12-19 13:54:12 -08:00
Leonardo de Moura
1ca8723c54
refactor(library/util): allow mk_telescopic_eq to be used with (terms, locals)
2014-12-19 13:54:12 -08:00
Leonardo de Moura
aedf74e80a
feat(util/list): add to_list from buffer
2014-12-19 13:54:12 -08:00
