Leonardo de Moura
|
191bfcddc1
|
chore: remove #exit
|
2020-02-24 19:32:57 -08:00 |
|
Leonardo de Moura
|
f84e1c2fbd
|
feat: add dummy implementation of MaxSharing primitives
|
2020-02-24 19:30:53 -08:00 |
|
Leonardo de Moura
|
37f52ab926
|
chore: update stage0
|
2020-02-24 19:24:44 -08:00 |
|
Leonardo de Moura
|
46fd5ed929
|
feat: maxSharing primitives
|
2020-02-24 19:23:45 -08:00 |
|
Leonardo de Moura
|
0781c74754
|
chore: variable order consistency
|
2020-02-24 18:29:24 -08:00 |
|
Leonardo de Moura
|
370dada9a3
|
feat: add findEntry? functions
|
2020-02-24 15:47:59 -08:00 |
|
Leonardo de Moura
|
c78ae90bda
|
chore: update stage0
|
2020-02-24 14:32:49 -08:00 |
|
Leonardo de Moura
|
d6a7e9a308
|
chore: remove mutquot primitives
|
2020-02-24 14:28:32 -08:00 |
|
Leonardo de Moura
|
a68249393a
|
chore: minimize dependencies
|
2020-02-24 13:18:07 -08:00 |
|
Leonardo de Moura
|
55e21e13cf
|
chore: remove broken MutQuot
`MutQuot.mk` primitive is affected by the polymorphic reference issue.
|
2020-02-24 13:03:16 -08:00 |
|
Leonardo de Moura
|
2be69f1d56
|
test: add new induction tactic tests
|
2020-02-23 19:30:33 -08:00 |
|
Leonardo de Moura
|
605edd05ae
|
feat: handle alternatives
|
2020-02-23 19:29:54 -08:00 |
|
Leonardo de Moura
|
7602cea77d
|
fix: add missing file
|
2020-02-23 19:29:42 -08:00 |
|
Leonardo de Moura
|
af4a88b615
|
chore: update stage0
|
2020-02-23 18:50:13 -08:00 |
|
Leonardo de Moura
|
b9dc76df35
|
feat: name minor premises using ctor names
|
2020-02-23 18:45:53 -08:00 |
|
Leonardo de Moura
|
a1303a6515
|
feat: use focusAux, and return new subgoals
|
2020-02-23 17:50:06 -08:00 |
|
Leonardo de Moura
|
d2801782de
|
fix: missing headBeta
|
2020-02-23 17:47:28 -08:00 |
|
Leonardo de Moura
|
6c34c3b14a
|
feat: add induction tactic
|
2020-02-23 17:23:52 -08:00 |
|
Leonardo de Moura
|
c4dac739be
|
feat: add support for user-defined recursors at getRecInfo
|
2020-02-23 12:42:08 -08:00 |
|
Leonardo de Moura
|
a5ad840ebe
|
feat: add getParamNames
|
2020-02-23 12:01:06 -08:00 |
|
Leonardo de Moura
|
e0fba69abc
|
chore: update stage0
|
2020-02-23 10:46:06 -08:00 |
|
Leonardo de Moura
|
346378b3a3
|
feat: add [recursor <major-pos>] attribute
|
2020-02-23 10:35:14 -08:00 |
|
Leonardo de Moura
|
325bb6b5b5
|
feat: helper function for user-defined recursors
|
2020-02-23 10:34:49 -08:00 |
|
Leonardo de Moura
|
72f57c923d
|
feat: helper functions for evalInduction
|
2020-02-22 19:57:44 -08:00 |
|
Leonardo de Moura
|
8baa376135
|
feat: allow _ at inductionAlt var names
|
2020-02-22 12:05:11 -08:00 |
|
Leonardo de Moura
|
472276f63f
|
feat: add mkRecFor
|
2020-02-22 11:24:46 -08:00 |
|
Leonardo de Moura
|
38cb8907a0
|
feat: add helper functions
|
2020-02-22 11:16:55 -08:00 |
|
Leonardo de Moura
|
4a8c192a00
|
feat: allow _ "else case" at inductionAlt
|
2020-02-22 11:16:20 -08:00 |
|
Leonardo de Moura
|
14b9e13dc1
|
fix: incorrect eraseMacroScopes
|
2020-02-22 11:16:05 -08:00 |
|
Leonardo de Moura
|
9abb749663
|
fix: preserve tag
|
2020-02-21 19:06:54 -08:00 |
|
Leonardo de Moura
|
09f504f376
|
feat: finish evalGeneralize
|
2020-02-21 18:32:00 -08:00 |
|
Leonardo de Moura
|
9e2d833be1
|
feat: add evalGeneralize
|
2020-02-21 13:42:51 -08:00 |
|
Leonardo de Moura
|
887c7524cc
|
chore: update stage0
|
2020-02-21 12:14:49 -08:00 |
|
Leonardo de Moura
|
96c7f794cc
|
feat: add generalize parser syntax
|
2020-02-21 12:12:41 -08:00 |
|
Leonardo de Moura
|
15e60e0e05
|
feat: add induction tactic entry point
|
2020-02-21 12:07:10 -08:00 |
|
Leonardo de Moura
|
021986fcad
|
chore: update stage0
|
2020-02-21 11:45:22 -08:00 |
|
Leonardo de Moura
|
bb0bfb5742
|
fix: sepBy
If parser consumed something, keep error.
|
2020-02-21 11:43:45 -08:00 |
|
Leonardo de Moura
|
9694102b3e
|
chore: update stage0
|
2020-02-21 11:32:04 -08:00 |
|
Leonardo de Moura
|
2fee8059b6
|
feat: add induction tactic parser
|
2020-02-21 11:30:36 -08:00 |
|
Leonardo de Moura
|
bc4b3047a9
|
feat: add whnfHeadPred and whnfUntil
|
2020-02-20 13:09:22 -08:00 |
|
Leonardo de Moura
|
731a0db044
|
test: add mkRecursorInfo tests
|
2020-02-19 19:08:03 -08:00 |
|
Leonardo de Moura
|
583984d044
|
feat: add getProduceMotiveAndRecursive and cleanup
|
2020-02-19 19:07:42 -08:00 |
|
Leonardo de Moura
|
3633ac117b
|
feat: add mkRecursorInfo
TODO: `getProduceMotiveAndRecursive`
|
2020-02-19 18:07:38 -08:00 |
|
Leonardo de Moura
|
d99e41b848
|
feat: add helper functions
|
2020-02-19 14:55:16 -08:00 |
|
Leonardo de Moura
|
36096abec0
|
feat: add Array.findIdxM? and Array.getIdx?
|
2020-02-19 14:54:55 -08:00 |
|
Leonardo de Moura
|
4e941b15ba
|
feat: add mkRecursorInfo skeleton
|
2020-02-19 10:56:08 -08:00 |
|
Leonardo de Moura
|
9b6dba1198
|
chore: update stage0
|
2020-02-18 20:36:32 -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 |
|