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

4132 commits

Author SHA1 Message Date
Leonardo de Moura
0918a599ae feat(*): builtin support for uint functions 
@kha The VM versions just throw exceptions. They are just stubs to
make sure we can compile Lean.
I implemented the uint functions in the new runtime, but there are a
few missing cases marked with TODO.
I needed these builtins to be able to compile the C++ generated code for
corelib.
 2019-02-01 17:04:24 -08:00
Leonardo de Moura
54f501594d chore(library/init/data/uint,library/init/data/usize): simplify 2019-02-01 15:41:55 -08:00
Leonardo de Moura
4fa06e38b2 chore(*): add skeleton for new builtin primitives, update src/boot 2019-02-01 14:03:03 -08:00
Leonardo de Moura
1a190021ce feat(library/Makefile.in): generate src/boot 2019-02-01 11:15:51 -08:00
Sebastian Ullrich
a823157338 fix(library/init/lean/expander): fix let expansion again 
Last bug in core.lean!
 2019-01-22 11:16:00 +01:00
Sebastian Ullrich
0846cc2aa0 fix(library/init/lean/elaborator): to_level 2019-01-22 11:16:00 +01:00
Sebastian Ullrich
9f90dbfd3d feat(library/init/lean/parser/syntax): improve syntax.get_pos for more error positions 2019-01-22 11:16:00 +01:00
Sebastian Ullrich
099354eb5f fix(library/init/lean/expander): expansion of parameterized let 2019-01-21 22:07:10 +01:00
Sebastian Ullrich
814ceb43fe fix(library/init/lean/parser/declaration): axiom, constant, what's the difference 2019-01-21 18:09:26 +01:00
Sebastian Ullrich
abf60e3242 feat(library/init/lean/elaborator): include 2019-01-21 18:09:18 +01:00
Sebastian Ullrich
53d9cb5358 fix(library/init/lean/elaborator): resolve idents after 'attribute' 2019-01-21 17:47:17 +01:00
Sebastian Ullrich
c22fbb5cde feat(library/init/lean,frontends/lean/vm_elaborator): set_option 2019-01-20 18:21:41 +01:00
Sebastian Ullrich
88534abccd fix(library/init/lean/expander): tuple element order 2019-01-20 16:41:46 +01:00
Sebastian Ullrich
b24796d98e feat(library/init/lean/elaborator): inaccessible 2019-01-20 16:41:33 +01:00
Sebastian Ullrich
69e363446d fix(library/init/lean/{parser/term,elaborator}): local notations override previous notations 2019-01-20 16:25:15 +01:00
Sebastian Ullrich
05bf392385 fix(library/init/lean/frontend): parser error positions 2019-01-20 16:24:12 +01:00
Sebastian Ullrich
fc7acc9898 fix(library/init/lean/elaborator): choice 2019-01-20 14:39:22 +01:00
Sebastian Ullrich
dcd3b3dc5d fix(library/init/lean/elaborator): section variables need to be preresolved as well 
In
```
section binary
variables {α : Type u} {β : Type v}
variable f : α → α → α
local infix * := f
def commutative        := ∀ a b, a * b = b * a
end binary
```
the expansion of `*` applies a macro scope to `f`, so we need to resolve it
before that
 2019-01-20 13:22:08 +01:00
Sebastian Ullrich
1708fc74f8 fix(library/init/lean/elaborator): structure instances 2019-01-19 15:35:11 +01:00
Sebastian Ullrich
a23df570fc fix(library/init/lean/elaborator): match 2019-01-17 19:57:00 +01:00
Sebastian Ullrich
3e8e823893 fix(frontends/lean/vm_elaborator): preserve internal name of section variables 2019-01-17 19:57:00 +01:00
Sebastian Ullrich
85cad3a7f1 fix(library/init/lean/elaborator): equation heads 2019-01-17 19:57:00 +01:00
Sebastian Ullrich
8cc35b854b feat(library/init/lean/{expander,elaborator}): variable(s) 2019-01-17 17:06:52 +01:00
Sebastian Ullrich
0923a2cbae refactor(library/init/lean/elaborator): avoid deprecated expr locals in new elaborator state 2019-01-17 12:29:44 +01:00
Sebastian Ullrich
c338245536 feat(library/init/lean/elaborator): implement the only part of open/export 2019-01-16 19:49:44 +01:00
Sebastian Ullrich
13781ed114 feat(library/init/lean/parser/token): numeric literals of more exotic bases 2019-01-16 19:39:30 +01:00
Sebastian Ullrich
2c4b566038 feat(frontends/lean/vm_elaborator): implement equations 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
a6d5af7387 feat(library/init/lean/expander): expand class and class inductive 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
246eecf155 fix(library/init/lean/elaborator): do not mangle attribute names (since they are not environment identifiers) 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
ca058a6d8e chore(library/init/lean/expander): simplify constant normalization 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
5ef30a9300 fix(library/init/lean/elaborator): have serialization 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
dce62fc190 fix(library/init/lean/expander): structural substitution instead of abstraction-application when applying notations 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
c17ba349f3 refactor(library/init/lean/parser/syntax): factor out syntax.(m)replace 2019-01-16 19:12:40 +01:00
Sebastian Ullrich
31588a1013 fix(library/init/lean/elaborator): do not attach position to app, nodes without pos data 2019-01-15 18:51:24 +01:00
Sebastian Ullrich
5660a8e690 feat(library/init/lean/elaborator): transmit position information 2019-01-15 18:28:35 +01:00
Sebastian Ullrich
1b565fcaa0 feat(library/init/lean/elaborator): simplistic support of export 2019-01-15 17:44:14 +01:00
Sebastian Ullrich
d444b5ef49 chore(library/init/core): move sorry_ax up (temporarily) to get error recovery sooner 2019-01-15 17:42:09 +01:00
Sebastian Ullrich
7dd21df59f fix(library/init/lean/elaborator): C++ expects the oldest variable first 2019-01-15 16:20:46 +01:00
Sebastian Ullrich
d0062691de feat(library/init/lean): implement init_quot 2019-01-15 15:06:51 +01:00
Sebastian Ullrich
6e64089123 feat(frontends/lean/structure_cmd): implement structure 2019-01-15 15:01:52 +01:00
Sebastian Ullrich
fc3a0403ab feat(library/init/lean/parser/declaration): implement structure field blocks that go beyond regular binder syntax 2019-01-15 15:00:34 +01:00
Sebastian Ullrich
7aa06338c9 feat(frontends/lean/vm_elaborator): implement inductive 2019-01-14 14:49:40 +01:00
Sebastian Ullrich
0945a87fbb fix(library/init/lean/elaborator): to_pexpr: explicitness modifiers 2019-01-14 14:48:49 +01:00
Sebastian Ullrich
3216b1a268 feat(library/init/lean/elaborator): implement instance/example 2019-01-12 15:10:00 +01:00
Sebastian Ullrich
84e9dd9b1a feat(library/init/lean/elaborator,frontends/lean/vm_elaborator): implement def/theorem/abbreviation 2019-01-12 15:10:00 +01:00
Sebastian Ullrich
49f580f190 feat(library/compiler/builtin,frontends/lean/vm_elaborator): add temporary expr.local primitive 
This makes it possible (or at least much easier) to interface with old
parser/elaborator code using local_consts for e.g. `def` parameters.
 2019-01-12 14:16:43 +01:00
Sebastian Ullrich
fec4502e0f feat(library/init/lean/parser/term): parse and expand sorry 2019-01-07 22:19:47 +01:00
Sebastian Ullrich
2b5f19677d feat(frontends/lean/vm_elaborator): elaborate #check 2019-01-07 22:19:47 +01:00
Sebastian Ullrich
aadf2eb5c1 fix(library/init/lean/elaborator): resolve_global: add missing name part, append root and open resolutions 2019-01-06 18:19:12 +01:00
Sebastian Ullrich
93b0c372e0 fix(library/init/lean/elaborator): reset namespace stack at end of namespace 2019-01-06 18:17:28 +01:00