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

4355 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
02b7f980b0 fix(library/num): bug in to_pos_num, missing test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-26 08:18:07 -07:00
Leonardo de Moura
99438f0ee0 chore(library): add 'universe polymorphism' to list of extra feat 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 23:00:50 -07:00
Jeremy Avigad
5eedca08ea refactor(library): set up and document standard/classical/hott imports 2014-08-25 22:57:55 -07:00
Jeremy Avigad
413517b86d fix(library): correct markdown directories, revise defaults for logic and data 2014-08-25 22:57:55 -07:00
Leonardo de Moura
9715d06f4a feat(library): minor cleanup, replace 'refl _' with 'rfl', define equivalence relation for sets 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 22:54:44 -07:00
Leonardo de Moura
c11fd6b0d2 fix(tests/lean/run): adjust tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 21:39:46 -07:00
Leonardo de Moura
3903be34a4 feat(frontends/lean): process theorem statement independently of proof, thus we have the same behavior in sequential and parallel compilation modes, closes #84 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 21:26:17 -07:00
Leonardo de Moura
800d3bd70a fix(doc/lean/tutorial): typos 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:22:15 -07:00
Leonardo de Moura
2c35696fed chore(README.md): remove link to Lean 0.1 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:20:56 -07:00
Leonardo de Moura
04d9eb17d1 feat(kernel/conveter): improve support for proof irrelevant in the converter 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:19:18 -07:00
Leonardo de Moura
4a9e48d249 feat(doc/authors.md): update authors.md page 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 11:00:45 -07:00
Leonardo de Moura
82a7de83cc feat(frontends/lean/pp_options): use a more effective get_distinguishing_pp_options 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 10:23:28 -07:00
Leonardo de Moura
42a8fb5965 chore(tests/lean/run/matrix): simplify same_dim_irrel proof 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 09:27:19 -07:00
Leonardo de Moura
60d5e87a66 test(tests/lean/run): add matrix test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-25 09:04:39 -07:00
Leonardo de Moura
cbc81ea6c5 chore(*): minimize dependencies on tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-24 19:58:48 -07:00
Leonardo de Moura
fbf13994d8 refactor(*): use + for concatenating format objects 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-24 09:35:25 -07:00
Leonardo de Moura
7cb2ca62f4 refactor(Makefile): do not use full path on makefile rules 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:28:34 -07:00
Leonardo de Moura
df3c1d8dd2 chore(README.md): minor correction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:17:47 -07:00
Leonardo de Moura
d3131298c3 fix(README.md): broken links 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:16:20 -07:00
Leonardo de Moura
eb794f7491 refactor(shell): remove obsolete tests 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:12:19 -07:00
Leonardo de Moura
06da0ebaaf refactor(library): rename Makefile.common to Makefile 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:10:39 -07:00
Leonardo de Moura
dbaf81e16d refactor(library): remove unnecessary 'standard' subdirectory 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 18:08:09 -07:00
Jeremy Avigad
505b93b7cb refactor(lean/examples/constable.lean): move to library/standard/logic/examples/nuprl_examples.lean 2014-08-23 17:55:00 -07:00
Jeremy Avigad
d0f0e58a85 refactor(library/standard/data/int): split basic.lean into basic.lean and order.lean 2014-08-23 17:53:02 -07:00
Jeremy Avigad
47a1c00a6d refactor(library/standard): collect notation in general_notation 2014-08-23 17:53:02 -07:00
Jeremy Avigad
ad969b4695 feat(library/standard/logic): add identities 2014-08-23 17:53:02 -07:00
Leonardo de Moura
df60ab4ada fix(frontends/lean/calc): allow calc_subst to be defined for multiple operators, allow calc cmds to be organized into namespaces, fixes #65 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 16:45:04 -07:00
Leonardo de Moura
2f699fa53a feat(*): make sections 'permanent', and add 'transient' contexts, closes #88 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 15:45:15 -07:00
Leonardo de Moura
b13851ba13 feat(frontends/lean): add kind and type to index, closes #89 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 12:39:59 -07:00
Leonardo de Moura
01736bf82a feat(util/sexpr/format): expose flatten 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-23 12:00:32 -07:00
Leonardo de Moura
e602c4ba49 feat(frontends/lean): change multicomment to /- ... -/ 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 17:55:13 -07:00
Leonardo de Moura
c5a44aca44 fix(frontends/lean/elaborator): do not expose type information produced when synthesizing class instances 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 17:07:12 -07:00
Leonardo de Moura
2ada3af405 fix(frontends/lean/info_manager): add instantiate method to synth_info_data, fixes #94 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 15:55:15 -07:00
Leonardo de Moura
a5f0593df1 feat(*): change inductive datatype syntax 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 15:46:10 -07:00
Leonardo de Moura
626cd952e7 test(tests/lean/run): add overload test 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 15:23:33 -07:00
Leonardo de Moura
01000ff7df feat(library): add typed_expr macro 
We use it to enforce that a let-variable has the expected type

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 11:26:06 -07:00
Leonardo de Moura
d4ac482d76 refactor(kernel): move annotation to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:38:10 -07:00
Leonardo de Moura
b746492ac8 refactor(library/simple_formatter): rename simple_formatter to print 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:32:08 -07:00
Leonardo de Moura
7d987df429 refactor(kernel/formatter): move simple_formatter to library 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-22 10:26:45 -07:00
Leonardo de Moura
fdd37fb1f3 chore(library/standard/data/sum): remove hints, they are not needed after the fix 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 21:44:02 -07:00
Jeremy Avigad
1fdc483ab9 fix(library/standard/data/int): remove misnamed file 2014-08-21 21:41:28 -07:00
Jeremy Avigad
02fba6e949 feat(library/standard/hott/fibrant.lean): add fibrant to library 2014-08-21 21:41:28 -07:00
Jeremy Avigad
05d0089381 feat(library/standard/sum.lean): add properties of sum 2014-08-21 21:41:28 -07:00
Jeremy Avigad
3afad10a72 feat(library/standard): add decidability of le for int 2014-08-21 21:41:28 -07:00
Leonardo de Moura
937c465685 fix(library/unifier): too much reduction 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 21:37:51 -07:00
Leonardo de Moura
c4cc837e34 refactor(library/standard): define abbreviations using '@' 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 18:39:38 -07:00
Leonardo de Moura
07bc0727e2 feat(frontends/lean): 'let [inline]' is the default 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 18:24:22 -07:00
Leonardo de Moura
0df87bae24 chore(library/standard/data/nat/div): remove TODO 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 17:58:03 -07:00
Leonardo de Moura
6cf73b51e2 fix(library/unifier): bug in occurs_check, the dependency may be eliminated by reducing term 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 17:56:18 -07:00
Leonardo de Moura
3498d7ad61 fix(frontends/lean/parser): missing identifier information, fixes #83 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
 2014-08-21 16:58:25 -07:00