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
Leonardo de Moura
c434066f45
feat: elabModifyOp
2020-02-18 19:57:55 -08:00
Leonardo de Moura
be8037973c
fix: missing eraseMacroScopes
2020-02-18 18:40:57 -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
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
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
c7fcb2c5a7
fix: missing ensureHasType
2020-02-18 09:12:31 -08:00
Leonardo de Moura
918bf029d4
feat: elaborate structure instance default values
2020-02-17 20:16:44 -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
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
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
47aba91c43
feat: error message when optParam and autoParam are used at fun
2020-02-13 17:57:12 -08:00
Leonardo de Moura
2fa19b5881
chore: cleanup
2020-02-13 16:39:36 -08:00
Leonardo de Moura
da3bf54ec7
feat: elaborate autoParams
...
cc @Kha
2020-02-13 16:24:50 -08:00
Leonardo de Moura
fd7727cf81
feat: helper functions for updating SourceInfo
2020-02-13 16:22:28 -08:00
Leonardo de Moura
44817b8488
feat: autoParam takes the Name of an auxiliary declaration of type Syntax
...
@Kha The `Name` (tactic name) approach used in Lean3 is not suitable
for Lean4. The issue is that we define tactics using macros, and in
most cases, the user doesn't even know the node id.
2020-02-13 15:09:42 -08:00
Leonardo de Moura
2507ce206e
feat: change auto param syntax
2020-02-13 11:56:24 -08:00
Leonardo de Moura
93de4ce7b3
feat: elaborate by
2020-02-13 11:45:51 -08:00
Leonardo de Moura
f041dd1aa1
feat: add by notation
2020-02-13 11:34:24 -08:00
Leonardo de Moura
cc2f84aa5d
fix: allow empty sequence at seq
2020-02-13 11:34:09 -08:00
