Leonardo de Moura
b379bca28b
chore: rename PtrEqResult.yes ==> PtrEqResult.yesEqual
2020-03-02 08:29:49 -08:00
Leonardo de Moura
0f8b59eed7
fix: typo Prop => Type
2020-02-29 11:22:17 -08:00
Leonardo de Moura
684554e979
feat: add PtrEqResult
2020-02-29 11:00:50 -08:00
Leonardo de Moura
94cfcbbefe
chore: withPtrEqSubsingleton ==> withPtrEqResult
2020-02-29 10:12:06 -08:00
Leonardo de Moura
d511ddfa9e
feat: add SemiDeciable and withPtrEqSubsingleton
2020-02-29 09:50:31 -08:00
Leonardo de Moura
090b1e664d
feat: rename maxSharing => shareCommon
2020-02-28 10:53:41 -08:00
Leonardo de Moura
cca90b5f9f
chore: simplify withPtrEqDecEq
2020-02-27 11:45:02 -08:00
Leonardo de Moura
b83691baa2
feat: compute fvarSubst
2020-02-27 10:58:46 -08:00
Leonardo de Moura
2719eaeb63
fix: closes #119
2020-02-27 08:10:29 -08:00
Leonardo de Moura
53b57af125
fix: dangling file
2020-02-25 14:33:54 -08:00
Leonardo de Moura
cfd7fc8a87
fix: message::get_text
...
It was still using the old representation.
2020-02-25 14:20:55 -08:00
Leonardo de Moura
7e96380711
chore: remove unnecessary import
2020-02-25 13:49:26 -08:00
Leonardo de Moura
7496296c1e
fix: "filler" fields
2020-02-25 13:49:18 -08:00
Leonardo de Moura
6ada62a3ee
feat: export helper functions
...
Motivation: prevent changes in the scalar fields layout from breaking
C++ code.
Ideally, we should do that for all constructors, and implement a tool
that creates the C++ functions automatically for us.
We don't do it because we will delete most of this code after we
finish the Lean4 transition.
2020-02-25 13:00:22 -08:00
Leonardo de Moura
191bfcddc1
chore: remove #exit
2020-02-24 19:32:57 -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
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
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
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
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
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
bb0bfb5742
fix: sepBy
...
If parser consumed something, keep error.
2020-02-21 11:43:45 -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
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
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
