michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
8044 commits 3 branches 0 tags 28 MiB
Commit graph

1553 commits

Author SHA1 Message Date
Floris van Doorn
da5f10ce63 feat(hott): minor fixes. allow the usage of numerals for trunc_index 2015-12-17 12:46:16 -08:00
Leonardo de Moura
61ecf018e9 feat(frontends/lean,library/tactic): add easy tactic parsing support for at ... and with ... 2015-12-17 12:18:32 -08:00
Leonardo de Moura
c824a0e050 chore(library,hott): enforce naming conventions 2015-12-17 11:36:58 -08:00
Leonardo de Moura
13419d1561 chore(hott/library): cleanup 2015-12-17 11:31:07 -08:00
Leonardo de Moura
42eda36225 chore(library/algebra/ordered_ring): use 'note' 2015-12-15 09:33:57 -08:00
Sebastian Ullrich
2185ee7e95 feat(library/tactic): make let tactic transparent, introduce new opaque note tactic 
The new let tactic is semantically equivalent to let terms, while `note`
preserves its old opaque behavior.
 2015-12-14 10:14:02 -08:00
Leonardo de Moura
193a9d8cde refactor(library/norm_num): avoid manual constant name initialization 
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt

Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.

We also have a python script for initializing the C++ name objects.
To use the script:
   - go to src/library
   - execute
       python ../../script/gen_constants_cpp.py constants.txt

It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.

I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.

I found an assertion violation at line 606. Could you take a look?

Best,
Leo
 2015-12-13 21:38:59 -08:00
Leonardo de Moura
e3a35ba4fd feat(frontends/lean): add 'with_attributes' tactical 
closes #494
 2015-12-13 18:27:44 -08:00
Leonardo de Moura
d4e49a8434 feat(library/tactic/intros_tactic): intro without argument should introduce a single variable 
see #695
 2015-12-13 16:28:39 -08:00
Leonardo de Moura
49eae56db4 test(library/theories/group_theory): test auto-include in the group theory library 2015-12-13 13:40:54 -08:00
Leonardo de Moura
ef546c5c5b refactor(library): use anonymous instance implicit arguments 2015-12-13 11:46:48 -08:00
Floris van Doorn
2325d23f68 feat(hott): port nat and int from the standard library 2015-12-09 12:36:11 -08:00
Floris van Doorn
46739c8b70 feat(hott/algebra): port abstract structures 2015-12-09 12:34:06 -08:00
Leonardo de Moura
1b80dc0df6 feat(library/data/real/basic): improve performance 2015-12-09 10:57:16 -08:00
Jacob Gross
ab91f8dd5f feat(library/data/set/basic): add sInter_insert 
add sInter supporting lemma
 2015-12-07 21:39:30 -08:00
Leonardo de Moura
50df6b5698 feat(frontends/lean): rename '[intro]' ==> '[intro!]' and '[backward]' ==> '[intro]' 2015-12-07 21:33:35 -08:00
Leonardo de Moura
041c1cbb17 feat(library/blast): add strategies "grind" and "core_grind" 2015-12-07 20:30:59 -08:00
Leonardo de Moura
48bc18d492 feat(library/blast/grinder/intro_elim_lemmas): add intro/elim lemmas validation 2015-12-07 18:43:15 -08:00
Leonardo de Moura
295b1d21f5 feat(frontends/lean): add '[intro]' and '[elim]' annotations 2015-12-07 18:43:15 -08:00
Leonardo de Moura
85379b7706 feat(library/blast/actions/simple_actions): make sure contradiction action works even if classical logic support is not enabled 
not (not (not a)) -> not a
 2015-12-07 09:30:14 -08:00
Leonardo de Moura
732a92de05 feat(frontends/lean): add 'simp' as shortcut for 'with_options [blast.strategy "simp"] blast' 2015-12-06 13:14:04 -08:00
Leonardo de Moura
b36ce49f2b fix(tests,doc): adjust tests to changes in the standard library 2015-12-05 23:52:16 -08:00
Leonardo de Moura
b94e31a72c refactor(library): remove algebra namespace 2015-12-05 23:50:01 -08:00
Daniel Selsam
7a117c45bf feat(init/setoid): tag equivalence relation 2015-12-05 11:54:27 -08:00
Leonardo de Moura
fa938bb94c feat(frontends/lean/decl_cmds): allow modifier to be provided after the 'attribute' keyword, test 'at' keyword 2015-12-05 11:50:08 -08:00
Daniel Selsam
934b502c6f refactor(algebra/numeral): prove lemmas incrementally 2015-12-05 08:56:56 -08:00
Daniel Selsam
2e4765482b fix(algebra/ring): fix names 2015-12-05 08:56:56 -08:00
Daniel Selsam
a04c28d4c9 refactor(library/algebra): construct simplifier sets incrementally 2015-12-04 18:28:56 -08:00
Leonardo de Moura
5da1b52e47 feat(library/blast/unit/unit_propagate): make sure unif_propagate works even if 'not' is marked as '[reducible]' 2015-12-04 16:49:21 -08:00
Leonardo de Moura
00e34683f2 feat(library/app_builder): (try to) address not-issue and other reducibility annotation related issues in the app_builder 2015-12-04 16:03:06 -08:00
Daniel Selsam
6e478696d2 feat(library/blast/unit): preprocessor placeholder 2015-12-04 08:30:04 -08:00
Daniel Selsam
2bf9989bd9 refactor(library/blast/unit): simplify module 2015-12-04 08:30:03 -08:00
Jacob Gross
dd6bed371a feat(library/data/set/basic): Added a supporting lemma for sUnion, which will be essential for proofs by induction on finite sets 2015-12-02 23:05:59 -08:00
Joe Hendrix
719a78d541 style(library/data/bv): Use syntax for dite 2015-12-02 23:01:26 -08:00
Joe Hendrix
3574ad1f11 style(library/data/bv): Simplify from_bv and bv_mul 2015-12-02 23:01:26 -08:00
Joe Hendrix
fd1999a97f feat(library/data/bv): Add signed/unsigned comparisons. 2015-12-02 23:01:26 -08:00
Joe Hendrix
5cf6e18af0 refactor(library/data/bv): Cleanup formatting inconsistencies 2015-12-02 23:01:26 -08:00
Joe Hendrix
3fddca81b5 feat(library/data/bv): Add preliminary bitvector ops. 2015-12-02 23:01:26 -08:00
Joe Hendrix
e4c839f362 feat(library/data/tuple): Add tuple combinators 2015-12-02 23:01:26 -08:00
Joe Hendrix
42afd89583 feat(library/data/list): Add additonal list combinators. 2015-12-02 23:01:26 -08:00
Joe Hendrix
63a17a3f48 feat(library/data/bool): Add bxor definition 2015-12-02 23:01:26 -08:00
Leonardo de Moura
5721bc13a7 feat(library/init/logic): annotate logical connectives as [no_pattern] 2015-11-24 18:48:22 -08:00
Leonardo de Moura
d240b06ba2 feat(library/init/logic): add new simp rules 2015-11-22 17:04:25 -08:00
Floris van Doorn
0537ef2bd9 chore(*): add me as author to files where I made nontrivial contributions 2015-11-22 14:21:26 -08:00
Floris van Doorn
482c68b387 feat(*/list): add some computation rules for lists in both libraries 2015-11-22 14:21:26 -08:00
Floris van Doorn
cc03ca9c6d fix(reserved_notation): make :: bind stronger than ++ 
this allows us to write l1 ++ a :: l2 without parentheses
 2015-11-22 14:21:26 -08:00
Floris van Doorn
5abc450fad feat(list): port list.basic from the standard library 2015-11-22 14:21:26 -08:00
Leonardo de Moura
564e8f947d refactor(library): cleanup 2015-11-22 14:10:02 -08:00
Leonardo de Moura
c49caf3740 feat(library/blast/congruence_closure): add support for user-defined congruence lemmas in the congruence closure module 2015-11-21 14:43:51 -08:00
Leonardo de Moura
5a98a2538c refactor(library): move basic simp/congr rules to init folder, delete some legacy files 2015-11-20 16:38:10 -08:00