max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
13466 commits 1 branch 0 tags 5.3 GiB
Commit graph

13466 commits

This branch
This branch
All branches
Author SHA1 Message Date
Leonardo de Moura
a115a1538b chore(library/vm/vm_io): style 2018-02-15 16:25:17 -08:00
Leonardo de Moura
1c9648a12d chore(library): remove dead constants 2018-02-15 16:17:43 -08:00
Leonardo de Moura
ac13f8b0f9 feat(library/system/io): add random number generator support in the io monad 
@aqjune @nunoplopes: See new tests at tests/lean/run/random.lean

We have two actions in `io`. By default, `io` uses the C++
random number generator, but we can force it to use a `std_gen` with
the action `set_rand_gen`.

def rand (lo : nat := std_range.1) (hi : nat := std_range.2) : io nat
def set_rand_gen : std_gen → io unit
 2018-02-15 16:12:08 -08:00
Leonardo de Moura
ddfbaa6c8d fix(library/init/data/nat/basic): missing lemma 2018-02-15 14:36:28 -08:00
Leonardo de Moura
f786d21b0f feat(library/system): basic support for random numbers 
@aqjune @nunoplopes: This commit adds basic support for random numbers.
It defines a random number generator interface, and an basic
implementation based on the Haskell one.
We can add more implementations in the future if neeeded.
The new test program has a few examples.

BTW, this is a pure Lean implementation.
If we need more performance we can provide an implementation
using C++.
 2018-02-15 14:36:28 -08:00
Leonardo de Moura
f048da4c98 refactor(library/init/data): replace char.zero_lt_d800 proof 
See issue https://github.com/leanprover/tc/issues/8

cc @dselsam
 2018-02-15 14:36:28 -08:00
Scott Morrison
0e6f496b8e chore(README.md) fixing link to download page 2018-02-15 11:36:12 +01:00
Mario Carneiro
57934479ef refactor(algebra/ordered_field): move theorems from discrete 
The theorems themselves are unchanged, although the proofs had to be reordered and changed a bit to accomodate.
Conflicts:

	library/init/algebra/ordered_field.lean
 2018-02-13 10:51:50 -08:00
Scott Morrison
5d094cf835 cleanup(init/meta/tactic) removing obsolete meta constants 2018-02-13 10:45:04 -08:00
Nuno Lopes
1a9962011d chore(style): fix cast style 2018-02-13 10:42:08 -08:00
Nuno Lopes
7b45d28e77 chore(unicode): use utf8 chars directly in strings 2018-02-13 10:42:08 -08:00
Nuno Lopes
c43ebd8bf7 fix(msvc): remove another \uXX char that was causing an infinite loop 2018-02-13 10:42:08 -08:00
Nuno Lopes
977e11f9be fix(warnings): fix warnings on VS. its now /W2 clean 2018-02-13 10:42:08 -08:00
Nuno Lopes
a9078dd13a fix(doc): link to MSVC build instructions 2018-02-13 10:40:53 -08:00
Leonardo de Moura
96e02613fc fix(library/compiler/simp_inductive): erase trivial structure bug 2018-02-11 11:43:05 -08:00
Leonardo de Moura
30cfcc0fa6 fix(library/compiler/inliner): missing reduction 2018-02-11 09:28:42 -08:00
Sebastian Ullrich
affe3463ab fix(frontends/lean/elaborator): fix assertion error: accidental mutation of a variable 2018-02-08 14:07:08 +01:00
Sebastian Ullrich
5736fda1ee chore(frontends/lean/elaborator): do not name mvars from { .. } catchall 
We already use the same names for the field mvars, which can be confusing during debugging
 2018-02-08 14:04:33 +01:00
Leonardo de Moura
3771748b4c chore(library/native): remove dead code 
The deleted code was not finished, and we are going to add a new IR
and compiler.
 2018-02-07 17:29:25 -08:00
Nuno Lopes
d01e2d7ae8 fix(msvc): change previous MSVC workaround to change the code less 2018-02-06 10:11:10 -08:00
Nuno Lopes
9c756e24d3 fix(crash) due to calling isalpha with signed char in get_indentatnion() 2018-02-06 10:11:10 -08:00
Nuno Lopes
5cee9f8279 fix(crash) due to calling isalpha/isalnum with signed char in is_id_first() and is_id_rest() 2018-02-06 10:11:10 -08:00
Nuno Lopes
1e03151412 fix(msvc): compiler warning 2018-02-06 10:11:10 -08:00
Nuno Lopes
c01c49d33f fix(msvc): compile with multi-thread libraries when needed 2018-02-06 10:11:10 -08:00
Nuno Lopes
6c9d77c6fc fix(msvc): compile with /Zc:implicitNoexcept- to avoid a few hundred warnigns 2018-02-06 10:11:10 -08:00
Nuno Lopes
02d254e25c build(msvc): disable shared libraries; not working at the moment 2018-02-06 10:11:10 -08:00
Nuno Lopes
a69541ab67 fix(msvc): crashes in getopt and read_dir 2018-02-06 10:11:10 -08:00
Nuno Lopes
a8021c2176 fix(msvc): bugfix for LEAN_DISPLAY macros 
tested with gcc, clang, and MSVC 15
 2018-02-06 10:11:10 -08:00
Nuno Lopes
36f19f1d6e fix(msvc): fix a few more compilation errors 2018-02-06 10:11:10 -08:00
Nuno Lopes
f234de1440 doc(msvc): improve intellisense instructions 2018-02-06 10:11:10 -08:00
Nuno Lopes
a8594c5bd0 fix(msvc): fix linking of .exe 2018-02-06 10:11:10 -08:00
Nuno Lopes
aeaa19ac44 fix(style): use static_cast 2018-02-06 10:11:10 -08:00
Nuno Lopes
caab1c58d2 fix(build): style 2018-02-06 10:11:10 -08:00
Nuno Lopes
8019914ad4 doc(msvc): add instructions on how to get Intellisense working 2018-02-06 10:11:10 -08:00
Nuno Lopes
46cfd33a1b fix(build): attempt to fix linux buildbots 2018-02-06 10:11:10 -08:00
Nuno Lopes
b984079449 fix(build): tentatively fix msys buildbot 2018-02-06 10:11:10 -08:00
Nuno Lopes
93374bb2bc fix(msvc): add a simple getopt() implementation 2018-02-06 10:11:10 -08:00
Nuno Lopes
7f920d9d37 fix(build): regression in linux build 2018-02-06 10:11:10 -08:00
Nuno Lopes
50bc3b0314 fix(msvc): fix compilation of vm_io.cpp 2018-02-06 10:11:10 -08:00
Nuno Lopes
c1a768b7a7 fix(msvc): further work on MSVC port 
only 7 files left
 2018-02-06 10:11:10 -08:00
Nuno Lopes
ac6a16ddba feat(msvc): further work on MSVC compatibility 2018-02-06 10:11:09 -08:00
Nuno Lopes
59b5a4a07a feat(build): add preliminary MSVC support 
Still doesn't build fully, but at least Intellisense sort of works now
 2018-02-06 10:11:09 -08:00
Sebastian Ullrich
fe2e95def3 fix(library/module_mgr): Revert "feat(library/module_mgr): save .olean files of non-dirty .lean files in server mode" 
This reverts commit 18c2e3739a.
The change introduced a bug where a .olean file may have been saved even if
the corresponding module had produced errors during processing, as long as these
errors were not part of the current region of interest.
 2018-02-05 14:36:27 +01:00
Sebastian Ullrich
4d5bd6d03c fix(frontends/lean/elaborator): fix build 2018-02-02 20:53:24 +01:00
Sebastian Ullrich
703d12d594 feat(frontends/lean/elaborator): do not execute tactics after error recovery 2018-02-02 08:58:53 -08:00
Sebastian Ullrich
b3262d53b4 feat(frontends/lean/elaborator): structure notation: fall back to inferring superclasses 2018-02-02 08:58:53 -08:00
Sebastian Ullrich
86e231e6c9 feat(frontends/lean/structure_cmd): make superclass fields inst implicit 2018-02-02 08:58:53 -08:00
Sebastian Ullrich
9f25cf665e feat(frontends/lean/elaborator): structure instance notation: allow implicit fields 2018-02-02 08:58:53 -08:00
Sebastian Ullrich
6eeb90c8fb chore(frontends/lean/elaborator): remove confusing assign_mvar method 2018-02-02 08:58:53 -08:00
Sebastian Ullrich
040748419f refactor(frontends/lean/elaborator): refactor and document structure instance notation code 2018-02-02 08:58:53 -08:00