Leonardo de Moura
|
8bacf54b6c
|
chore: fix test
|
2020-02-24 21:03:40 -08:00 |
|
Leonardo de Moura
|
2be69f1d56
|
test: add new induction tactic tests
|
2020-02-23 19:30:33 -08:00 |
|
Leonardo de Moura
|
a5ad840ebe
|
feat: add getParamNames
|
2020-02-23 12:01:06 -08:00 |
|
Leonardo de Moura
|
09f504f376
|
feat: finish evalGeneralize
|
2020-02-21 18:32:00 -08:00 |
|
Leonardo de Moura
|
731a0db044
|
test: add mkRecursorInfo tests
|
2020-02-19 19:08:03 -08:00 |
|
Leonardo de Moura
|
ef747196d7
|
fix: structure instance parser
Use `fieldIndex` instead of `numLit`
|
2020-02-18 20:27:04 -08:00 |
|
Leonardo de Moura
|
0c13445da6
|
fix: mkStructView
Reamrk: `1.2` is a numLit
|
2020-02-18 20:22:04 -08:00 |
|
Leonardo de Moura
|
c434066f45
|
feat: elabModifyOp
|
2020-02-18 19:57:55 -08:00 |
|
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 |
|
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
|
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
|
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
|
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
|
47aba91c43
|
feat: error message when optParam and autoParam are used at fun
|
2020-02-13 17:57:12 -08:00 |
|
Leonardo de Moura
|
da3bf54ec7
|
feat: elaborate autoParams
cc @Kha
|
2020-02-13 16:24:50 -08:00 |
|
Leonardo de Moura
|
93de4ce7b3
|
feat: elaborate by
|
2020-02-13 11:45:51 -08:00 |
|
Leonardo de Moura
|
4227d3bce4
|
chore: reduce problem size
Motivation: avoid stack overflow in debug mode
|
2020-02-12 21:27:34 -08:00 |
|
Leonardo de Moura
|
263d22576b
|
test: add new implicit lambda test
|
2020-02-12 13:47:54 -08:00 |
|
Leonardo de Moura
|
1fe92ade36
|
doc: document why example fails
|
2020-02-12 13:46:55 -08:00 |
|
Leonardo de Moura
|
6c16deded4
|
feat: improve implicit lambdas
|
2020-02-12 13:38:01 -08:00 |
|
Leonardo de Moura
|
fc404af645
|
feat: solve ?m t =?= c even when constApprox is disabled
|
2020-02-12 13:21:56 -08:00 |
|
Leonardo de Moura
|
98c925ed7e
|
feat: elaborate #check_failure
|
2020-02-12 11:55:02 -08:00 |
|
Leonardo de Moura
|
17dfe3fb66
|
test: implicit lambda tests
|
2020-02-11 21:21:21 -08:00 |
|
Leonardo de Moura
|
41baf46083
|
feat: propagate expected type at elabFunCore
|
2020-02-11 17:47:51 -08:00 |
|
Leonardo de Moura
|
97dfe95b41
|
chore: fix test
and document why better expected type propagation broke this example.
|
2020-02-11 16:26:39 -08:00 |
|
Leonardo de Moura
|
2f959e23ca
|
fix: checkAssignment was overwriting assignment
|
2020-02-11 16:11:56 -08:00 |
|
Leonardo de Moura
|
55231b960e
|
feat: simplify and improve processAssignmentFOApproxAux
|
2020-02-11 14:42:02 -08:00 |
|
Leonardo de Moura
|
30e0ccd8c4
|
feat: implicit lambdas
It is still work in progress
|
2020-02-11 13:43:05 -08:00 |
|
Leonardo de Moura
|
03b5b7d562
|
feat: implicit lambdas
|
2020-02-11 09:59:46 -08:00 |
|
Leonardo de Moura
|
adb940e879
|
feat: new test
|
2020-02-11 09:34:45 -08:00 |
|
Leonardo de Moura
|
7085072590
|
feat: allow implicitBinder and instBinder at fun
|
2020-02-11 08:26:10 -08:00 |
|
Leonardo de Moura
|
f6ae8560e8
|
fix: isDefEq issue exposed by new test
|
2020-02-10 23:46:17 -08:00 |
|
Leonardo de Moura
|
f39586a237
|
test: expose problem at isDefEq
|
2020-02-10 22:22:42 -08:00 |
|
Leonardo de Moura
|
e732eac899
|
fix: but at elimMVarDepsApp
|
2020-02-10 20:49:43 -08:00 |
|
Leonardo de Moura
|
f0e2a3cfa4
|
chore: add small test
|
2020-02-10 20:37:37 -08:00 |
|
Leonardo de Moura
|
34776c4f41
|
chore: fix test
|
2020-02-10 14:48:57 -08:00 |
|
Leonardo de Moura
|
d37eb896ef
|
doc: performance issue
cc @dselsam
|
2020-02-10 14:40:48 -08:00 |
|