Leonardo de Moura
|
3da95ea8b0
|
test: structure instance tests
|
2020-02-18 17:50:42 -08:00 |
|
Leonardo de Moura
|
ae19d59d28
|
feat: add elabChoice for CommandElab
|
2020-02-18 17:18:28 -08:00 |
|
Leonardo de Moura
|
412c3f5978
|
feat: add evalChoice
cc @Kha
|
2020-02-18 16:31:36 -08:00 |
|
Leonardo de Moura
|
5a44227f73
|
fix: isModifyOp?
|
2020-02-18 11:35:13 -08:00 |
|
Leonardo de Moura
|
2f7976c317
|
chore: update stage0
|
2020-02-18 10:59:29 -08:00 |
|
Sebastian Ullrich
|
86d2b82c29
|
refactor: get rid of antiquotExpr hack
|
2020-02-18 10:57:27 -08:00 |
|
Sebastian Ullrich
|
25f764daad
|
feat: antiquotation escapes
|
2020-02-18 10:57:12 -08:00 |
|
Daniel Selsam
|
13721cdfe9
|
doc: elabissue for structure same-name error msg
|
2020-02-18 10:52:44 -08:00 |
|
Leonardo de Moura
|
7d7cd1a7c9
|
doc: document issue
cc @dselsam
|
2020-02-18 10:52:12 -08:00 |
|
Daniel Selsam
|
94e45f7b81
|
doc: elabissue for '<id>_main already defined' msg
|
2020-02-18 10:49:40 -08:00 |
|
Leonardo de Moura
|
36ea3fbaf7
|
doc: document issue
cc @dselsam
|
2020-02-18 10:49:04 -08:00 |
|
Leonardo de Moura
|
6900577723
|
doc: document issue
AFAICT, it has been solved in the new frontend. See new test.
cc @dselsam
|
2020-02-18 10:41:12 -08:00 |
|
Daniel Selsam
|
1981bbbc7c
|
doc: elabissue for two improvable error messages
|
2020-02-18 10:34:24 -08:00 |
|
Leonardo de Moura
|
50ddb98fb4
|
chore: update stage0
|
2020-02-18 10:29:59 -08:00 |
|
Leonardo de Moura
|
86faccca72
|
fix: structure instance parser
|
2020-02-18 10:28:43 -08:00 |
|
Leonardo de Moura
|
f8c73ba95d
|
fix: missing ensureHasType
|
2020-02-18 10:09:22 -08:00 |
|
Leonardo de Moura
|
dcd64fae5a
|
test: add new structure instance + implicit lambda tests
|
2020-02-18 09:18:52 -08:00 |
|
Leonardo de Moura
|
c7fcb2c5a7
|
fix: missing ensureHasType
|
2020-02-18 09:12:31 -08:00 |
|
Leonardo de Moura
|
ba93e9b895
|
chore: update stage0
|
2020-02-17 20:17:40 -08:00 |
|
Leonardo de Moura
|
918bf029d4
|
feat: elaborate structure instance default values
|
2020-02-17 20:16:44 -08:00 |
|
Leonardo de Moura
|
81d8b75dff
|
doc: Lean3 structure instance bugs
|
2020-02-17 20:12:06 -08:00 |
|
Leonardo de Moura
|
378dca293e
|
test: add Expr.find? test
|
2020-02-17 19:49:13 -08:00 |
|
Leonardo de Moura
|
09f613111b
|
perf: remove used field
The trick is to use `()` to initialize `keys`.
`()` is not a valid `Expr` in our runtime.
|
2020-02-17 19:18:59 -08:00 |
|
Leonardo de Moura
|
ba61c9866c
|
feat: add FindExpr
|
2020-02-17 19:13:40 -08:00 |
|
Leonardo de Moura
|
386e6179ff
|
fix: missing [inline] and code idioms that produce low performance code
|
2020-02-17 19:06:42 -08:00 |
|
Leonardo de Moura
|
36b723193c
|
refactor: move ReplaceExpr to Init/Lean/Util
|
2020-02-17 18:41:13 -08:00 |
|
Leonardo de Moura
|
802f4d4d27
|
feat: add reduceProj?
|
2020-02-17 18:33:59 -08:00 |
|
Leonardo de Moura
|
00043a4903
|
feat: default field synthesis skeleton
|
2020-02-17 16:33:30 -08:00 |
|
Leonardo de Moura
|
ca20bb112f
|
feat: add helper
|
2020-02-17 12:10:52 -08:00 |
|
Leonardo de Moura
|
bd951b40ce
|
refactor: remove unnecessary complexity
|
2020-02-17 11:43:55 -08:00 |
|
Leonardo de Moura
|
9b23c6cd10
|
feat: elaborate fields
TODO: `default values`
|
2020-02-17 11:34:50 -08:00 |
|
Leonardo de Moura
|
57ee977291
|
feat: add helper functions
|
2020-02-17 11:28:50 -08:00 |
|
Leonardo de Moura
|
b497c7e6a7
|
feat: add missing fields
|
2020-02-16 12:45:11 -08:00 |
|
Leonardo de Moura
|
6a80410917
|
fix: getStructName
|
2020-02-16 11:24:55 -08:00 |
|
Leonardo de Moura
|
4101ba640c
|
chore: add resolveGlobalName method
|
2020-02-16 11:17:53 -08:00 |
|
Leonardo de Moura
|
8e4f3beff3
|
chore: fix test
|
2020-02-15 16:15:37 -08:00 |
|
Leonardo de Moura
|
1c8baa0198
|
feat: add withPtrEqDecEq (version of withPtrEq for implementing decidable equality)
cc @dselsam
|
2020-02-15 16:12:09 -08:00 |
|
Leonardo de Moura
|
db3d9c9284
|
feat: helper theorems
|
2020-02-15 16:08:43 -08:00 |
|
Leonardo de Moura
|
3ebb4e76ee
|
feat: more general withPtrEq
|
2020-02-15 15:53:30 -08:00 |
|
Leonardo de Moura
|
d0c866e0d5
|
chore: update stage0
|
2020-02-15 15:48:05 -08:00 |
|
Leonardo de Moura
|
932f4a7646
|
chore: update stage0
|
2020-02-15 15:44:21 -08:00 |
|
Leonardo de Moura
|
148c0324c4
|
fix: do not extract closed terms from join point applications
|
2020-02-15 15:43:24 -08:00 |
|
Leonardo de Moura
|
dd4fac2a7b
|
chore: helper functions
|
2020-02-14 21:02:59 -08:00 |
|
Leonardo de Moura
|
9e68c1e1c6
|
feat: add generalize and replaceLocalDecl
|
2020-02-14 20:06:56 -08:00 |
|
Leonardo de Moura
|
203bf08339
|
refactor: try ==> commitWhen
|
2020-02-14 19:17:11 -08:00 |
|
Leonardo de Moura
|
ddf6ecaea3
|
chore: remove dead code
|
2020-02-14 19:11:15 -08:00 |
|
Leonardo de Moura
|
551f6ebcd0
|
feat: rewriteCore tactic
|
2020-02-14 09:40:29 -08:00 |
|
Leonardo de Moura
|
c30c14ec84
|
chore: update stage0
|
2020-02-13 18:27:58 -08:00 |
|
Leonardo de Moura
|
0cf226220c
|
fix: remove incorrect assertion
Note that `get_cases_on_minors_range` is now parametric on `m_before_erasure`:
`get_cases_on_minors_range(env(), const_name(fn), m_before_erasure)`
|
2020-02-13 18:26:12 -08:00 |
|
Leonardo de Moura
|
47aba91c43
|
feat: error message when optParam and autoParam are used at fun
|
2020-02-13 17:57:12 -08:00 |
|