Leonardo de Moura
f546b13b6c
fix(library/init/lean/syntax): setTailInfo, getHeadInfo and getTailInfo
2019-08-08 20:55:29 -07:00
Leonardo de Moura
9937855d89
feat(library/init/lean/parser/transform): add removeParen
2019-08-08 20:35:00 -07:00
Leonardo de Moura
98b0167e27
chore(library/init/lean/parser/parser): fix typo
2019-08-08 20:34:33 -07:00
Leonardo de Moura
d8f295d980
feat(library/init/lean): helper functions for transforming Syntax objects
2019-08-08 20:11:57 -07:00
Leonardo de Moura
a2956f5bd6
feat(library/init/lean/syntax): add mrewriteBottomUp and rewriteBottomUp
2019-08-08 18:58:43 -07:00
Leonardo de Moura
c6795996f6
feat(library/init/lean/parser/term): allow match syntax to be used in def
2019-08-08 18:53:51 -07:00
Leonardo de Moura
849311af00
test(tests/playground/patch): do-nothing transformer
2019-08-08 10:47:19 -07:00
Leonardo de Moura
10a8822ac5
fix(library/init/lean/parser/module): use updateLeading
2019-08-08 10:45:15 -07:00
Leonardo de Moura
74c46d2b35
fix(library/init/lean/parser/parser): symbolNoWs was not creating an atom
2019-08-08 10:41:40 -07:00
Leonardo de Moura
7a89d45391
feat(script): add helper script for patching lean files
2019-08-08 10:20:32 -07:00
Leonardo de Moura
6b0eb79d37
feat(library/init/lean/parser/module): add convenient parseFile function for writing syntax "patching" tools
2019-08-08 09:42:57 -07:00
Leonardo de Moura
30fc07014e
chore(stage0): update
2019-08-07 17:46:48 -07: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
bf2a365501
chore(library/compiler/compiler): remove dead code
2019-08-07 17:24:07 -07:00
Leonardo de Moura
748e272dcb
chore(stage0): update
2019-08-07 17:20:40 -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
4cff63af3f
chore(library/init/lean/environment): remove dead comment
2019-08-07 16:31:01 -07:00
Leonardo de Moura
d707026cd8
feat(library/local_context): ensure local_context is just a wrapper for LocalContext
...
This is a temporary hack. After we eliminate the old elaborator,
we will delete the C++ class `local_context`.
In Lean4, we will not have two different kinds of local context:
`local_ctx` and `local_context`.
2019-08-07 13:11:08 -07:00
Leonardo de Moura
8ac58a66f8
chore(library/abstract_type_context): remove unnecessary virtual method only used at old pp.cpp
2019-08-07 12:05:10 -07:00
Leonardo de Moura
fcba361bdf
chore(stage0): update
2019-08-07 11:56:17 -07:00
Leonardo de Moura
ae97cfdd68
feat(kernel/local_ctx): use LocalContext
2019-08-07 11:50:20 -07:00
Leonardo de Moura
c9fa63edad
feat(library/init/lean/localcontext): add LocalContext.mfor
2019-08-07 11:39:51 -07:00
Leonardo de Moura
d5707bb256
fear(library/init/data/persistentarray/basic): add PersistentArray.mfor
2019-08-07 11:33:44 -07:00
Leonardo de Moura
1b5fc0e2c1
fix(library/init/data/array/basic): incorrect universe level
2019-08-07 11:33:23 -07:00
Leonardo de Moura
3967496ac9
chore(library/init/lean/default): make sure new modules are initialized
2019-08-07 07:14:09 -07:00
Leonardo de Moura
7a2ac23497
chore(library/init/lean/localcontext): export functions
2019-08-06 18:14:03 -07:00
Leonardo de Moura
1d597d462d
chore(library/init/lean): minor
2019-08-06 17:55:09 -07:00
Leonardo de Moura
bad3f8e77e
chore(kernel/local_ctx): use new representation defined at localcontext.lean
2019-08-06 10:47:50 -07:00
Leonardo de Moura
2343260ca5
chore(stage0): update
2019-08-06 10:39:02 -07:00
Leonardo de Moura
b27f215b9a
chore(library/local_context): simplify pp
2019-08-06 10:27:10 -07:00
Leonardo de Moura
81854a2d25
feat(library/init/lean/metavarcontext): add MetavarContext
2019-08-06 10:17:40 -07:00
Leonardo de Moura
f1eaebba31
fix(library/compiler/csimp): bug at float_cases_on
...
The scope of the expr2ctor cache updates was incorrect.
This bug affects code of the form
```
let x := C.cases_on y ...; K[x]
```
when we try to float the `cases_on` application, and the continuation
`K[x]` contains another `cases_on` application with major `y`.
The new test exposes the bug.
This commit also fixes the case where the continuation `K[x]` projects `y`.
Fixes #26
2019-08-05 13:23:27 -07:00
Leonardo de Moura
99e90f0410
chore(library/compiler): add trace.compiler.simp_float_cases option
2019-08-05 13:13:18 -07:00
Leonardo de Moura
fb5fb03f00
feat(library/init/lean/localcontext): add isSubPrefixOf
2019-08-05 09:44:20 -07:00
Leonardo de Moura
215a3ac8fd
chore(library/tactic/clear_tactic): remove dead code
2019-08-05 08:58:59 -07:00
Leonardo de Moura
3ecf8ac8ec
feat(library/init/data/persistentarray/basic): add mfoldlFrom and foldlFrom
2019-08-05 07:41:41 -07:00
Leonardo de Moura
bb8b13d240
chore(tests/compiler/expr): fix test output
2019-08-04 13:30:11 -07:00
Leonardo de Moura
1b426db5d9
chore(stage0): update
2019-08-04 13:25:25 -07:00
Leonardo de Moura
34024256ab
chore(library/init/lean/expr): simplify Expr.mvar constructor
2019-08-04 13:24:27 -07:00
Leonardo de Moura
142063fee4
feat(library/init/lean/localcontext): add getUnusedName
2019-08-04 13:14:22 -07:00
Leonardo de Moura
2a914d99dd
feat(library/init/lean/localcontext): missing functions
2019-08-04 13:01:01 -07:00
Leonardo de Moura
af46e36266
fix(library/init/data/persistentarray/basic): universes
2019-08-04 13:00:32 -07:00
Leonardo de Moura
2a58e58480
feat(library/init/data/persistentarray/basic): add mfind and mfindRev
2019-08-04 12:30:12 -07:00
Leonardo de Moura
c1e36fbaec
feat(library/init/lean/localcontext): add erase and pop
2019-08-04 11:58:53 -07:00
Leonardo de Moura
4bd347de3a
feat(library/init/data/persistentarray/basic): PersistentArray.pop
2019-08-04 11:50:05 -07:00
Leonardo de Moura
4181f35546
chore(stage0): update
2019-08-04 09:30:52 -07:00
Leonardo de Moura
f55a00a022
feat(library/init/lean): add LocalContext
2019-08-04 09:29:05 -07:00
Leonardo de Moura
8a8b45b6e0
chore(stage0): update
2019-08-04 08:41:19 -07:00
Leonardo de Moura
c5abab8fd2
fix(library/init/lean/path): <dir>/<mod>.lean must have precedence over <dir>/<mod>/default.lean
2019-08-04 08:38:48 -07:00
Leonardo de Moura
1ef23950a4
chore(library/init/lean/expr): expose temporary legacy constructor
2019-08-04 08:03:09 -07:00
