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

44 commits

Author SHA1 Message Date
Leonardo de Moura
411f397654 refactor(library/init/data/list): new name convention for List functions 
cc @dselsam @kha
 2019-10-01 15:15:02 -07:00
Leonardo de Moura
18e6a106f4 feat(library/init/lean/smap): implement SMap using PHashMap instead of RBMap 2019-09-20 14:22:03 -07:00
Leonardo de Moura
02e4abb24a feat(library/init/lean/elaborator): convertForall skeleton 2019-09-17 17:17:46 -07:00
Leonardo de Moura
2996d306c9 feat(library/init): add more general modify: modifyGet 
This commit also adds a few helper elaboration functions.
 2019-09-16 15:14:02 -07:00
Leonardo de Moura
b2693962bd chore(library/init/lean): export as C functions 2019-08-17 07:30:07 -07:00
Leonardo de Moura
e1588c3fe7 feat(library/init/lean/elaborator): add expected type 2019-08-14 07:16:24 -07:00
Leonardo de Moura
d002e550bb chore(library/init/lean): filename ==> fileName 2019-08-13 19:51:04 -07:00
Leonardo de Moura
13a67cb9a7 feat(library/init/lean/elaborator/preterm): add glue code for new and old elaborators 2019-08-13 19:42:41 -07:00
Leonardo de Moura
03e455d32d feat(frontends/lean/elaborator): add oldElaborate 2019-08-13 19:23:29 -07:00
Leonardo de Moura
6a6758edf8 refactor(library/init/lean/elaborator): move elabTerm to term.lean 2019-08-13 18:33:42 -07:00
Leonardo de Moura
cbcf2a8a49 feat(library/init/lean/elaborator): arrow, hole and sorry 2019-08-13 15:14:51 -07:00
Leonardo de Moura
e16288136b fix(library/init/lean/elaborator/basic): logErrorAndThrow should not log error twice 2019-08-13 13:24:00 -07:00
Leonardo de Moura
cea1fa3036 feat(library/init/lean/elaborator/command): display position information at #resolve_name 2019-08-11 15:59:10 -07:00
Leonardo de Moura
3dad81daee feat(library/init/lean/elaborator): add resolvename.lean 2019-08-11 15:37:37 -07:00
Leonardo de Moura
d00019f57e chore(library/init): fix whitspaces before => 2019-08-09 09:13:49 -07:00
Sebastian Ullrich
3ed67138d5 chore(*): update equation syntax in files and old parser 
for f in ../../**/*.lean; do echo $f; ./patch.lean.out $f > tmp && cat tmp > $f; done
 2019-08-09 11:11:34 +02:00
Leonardo de Moura
6e4b9f2cc1 feat(library/init/lean/elaborator/command): elaborate init_quot command 2019-08-07 17:41:18 -07:00
Leonardo de Moura
73f96730bb feat(library/init/lean,kernel): add KernelException, addDecl and compileDecl 
This commit also refines the type of `addAndCompile`.
We also add `ElabException.kernel` constructor for kernel exceptions.
 2019-08-07 17:15:40 -07:00
Leonardo de Moura
bfb5bd3752 feat(library/init/lean/elaborator): add universe and universes elaborators 2019-07-31 16:46:02 -07:00
Leonardo de Moura
46f361daab feat(library/init/lean/elaborator): add open command elaborator 2019-07-31 15:58:04 -07:00
Leonardo de Moura
66a93dbb39 feat(library/init/lean/elaborator/basic): absolutizeModuleName 2019-07-27 18:17:21 -07:00
Leonardo de Moura
c1e217da2b feat(library/init/lean/path): absolutizeModuleName 2019-07-26 17:26:44 -07:00
Leonardo de Moura
5a1380ec6a feat(library/init/lean): add lean/path.lean 2019-07-25 19:28:22 -07:00
Leonardo de Moura
3145994e36 feat(library/init/lean/elaborator/basic): register declaration name prefixes as namespaces at Environment.add 2019-07-24 13:24:02 -07:00
Leonardo de Moura
cf8daf4b24 feat(library/init/lean/elaborator): process header 
TODO:
- improve/fix `setSearchPath`
- add `IO.getEnv`
- add support for relative imports at `absolutizeModuleName`
 2019-07-24 07:37:33 -07:00
Leonardo de Moura
b792afb9d5 feat(library/init/lean/elaborator): add root scope and resolveNamespace 2019-07-23 09:14:01 -07:00
Leonardo de Moura
b5d4e0a2fd chore(library/init/lean/elaborator/basic): improve cryptic error message 2019-07-22 19:07:43 -07:00
Leonardo de Moura
39b5fbb767 feat(library/init/lean/elaborator): registerNamespace 2019-07-22 18:47:25 -07:00
Leonardo de Moura
3609057848 feat(library/init/lean/elaborator/basic): add OpenDecl 2019-07-22 17:40:37 -07:00
Leonardo de Moura
2387f3c2a2 feat(library/init/lean/elaborator): improve namespace, scope, and end commands 2019-07-22 08:14:35 -07:00
Leonardo de Moura
eb47746647 feat(library/init/lean/elaborator): namespace, section and end commands 2019-07-21 16:55:23 -07:00
Leonardo de Moura
fdb2fb3f0d chore(library/init/lean): add helper function 2019-07-21 08:21:20 -07:00
Leonardo de Moura
a535d348de feat(library/init/lean/elaborator): use SyntaxNode to define TermElab and CommandElab 2019-07-21 07:29:41 -07:00
Leonardo de Moura
fdbbdf68fc refactor(library/init/lean/elaborator/basic): make sure ElabState does not depend on parser state 
cc @kha
 2019-07-19 17:07:39 -07:00
Leonardo de Moura
b3e0a1d04e feat(library/init/lean/elaborator/basic): improve error handling, add simple test 2019-07-18 17:52:01 -07:00
Leonardo de Moura
eb7b2b77fa chore(library/init/lean): minor changes 2019-07-18 17:16:44 -07:00
Leonardo de Moura
99c465b425 feat(library/init/lean/elaborator/basic): add basic error handling functions 2019-07-18 16:37:39 -07:00
Leonardo de Moura
d92cd91ab3 feat(library/init/lean/elaborator/basic): add processCommand and test function 2019-07-18 16:12:18 -07:00
Leonardo de Moura
4e94bdae48 feat(library/init/lean/elaborator/basic): add [elabTerm] and [elabCommand] attributes 2019-07-18 15:27:27 -07:00
Leonardo de Moura
0f1f23744e chore(library/init/lean/elaborator/basic): examples 2019-07-17 19:09:16 -07:00
Leonardo de Moura
bccad07718 feat(library/init/lean/elaborator/basic): add [builtinCommandElab] attribute 2019-07-17 19:09:16 -07:00
Leonardo de Moura
2f7220402d chore(stage0): update 2019-07-17 19:09:16 -07:00
Leonardo de Moura
21e973aeaf feat(library/init/lean/elaborator/basic): add [builtinTermElab] attribute 2019-07-17 19:09:16 -07:00
Leonardo de Moura
eebb8e2e27 feat(library/init/lean/elaborator): add Elab monad 2019-07-17 19:09:16 -07:00