Leonardo de Moura
fc1e4cb533
feat: add Array.isPrefixOf
2020-09-08 14:40:43 -07:00
Leonardo de Moura
ecda364985
feat: add Expr.forEach
2020-09-08 13:03:53 -07:00
Leonardo de Moura
9151fef49d
feat: abstract proofs occurring in binders
2020-09-08 12:29:35 -07:00
Leonardo de Moura
ebe2cf272e
feat: add MonadCacheT
2020-09-08 10:48:47 -07:00
Leonardo de Moura
722608d0c6
chore: fix test
2020-09-07 16:35:28 -07:00
Leonardo de Moura
b6079e12b8
feat: expand macros infix, infixl, infixr, prefix, and postfix
2020-09-07 16:35:25 -07:00
Leonardo de Moura
fded18d114
chore: mkElim ==> mkMatcher
2020-09-07 14:33:39 -07:00
Leonardo de Moura
91363bae19
feat: improve resolveLVal
2020-09-07 12:25:43 -07:00
Leonardo de Moura
7809fe0b01
fix: def+match macro
2020-09-07 11:34:53 -07:00
Leonardo de Moura
a12bc273bb
refactor: src/Lean/Meta/EqnCompiler ==> src/Lean/Meta/Match
2020-09-07 11:09:48 -07:00
Leonardo de Moura
ddf12c91c2
fix: do not consider auxiliary declarations as local instances
2020-09-07 08:08:35 -07:00
Leonardo de Moura
79130bc3f9
feat: add addAndCompilePartial
2020-09-07 07:56:11 -07:00
Leonardo de Moura
81582e4482
feat: break PreDefinitions into strongly connected components
2020-09-06 14:22:06 -07:00
Leonardo de Moura
56e6b9b398
feat: add Tarjan's SCC
2020-09-06 14:19:59 -07:00
Leonardo de Moura
6704468f07
feat: add coeId instance
...
Add an example showing why it is useful.
TODO: reconsider whether we should use the approximation described in
the new test or not.
2020-09-06 08:27:26 -07:00
Leonardo de Moura
102d2ae57d
fix: avoid unnecessary reduction
...
```lean
forallBoundedTelescope `(Nat -> IO Nat) 1 fun xs type => ...
```
should assign `IO Nat` to `type` instead of `IO.RealWorld -> ...`
2020-09-06 06:57:52 -07:00
Leonardo de Moura
3ae3c51a8c
feat: add Array.partition
2020-09-05 08:48:15 -07:00
Leonardo de Moura
70c42456b9
feat: expand intro+matchAlts macro
2020-09-04 18:22:56 -07:00
Leonardo de Moura
ef64e1c25a
feat: fun+match macro
...
Example:
```
fun
| 0 => true
| _ => false
```
2020-09-04 16:23:01 -07:00
Leonardo de Moura
3dbd2b728b
feat: add Array.getMax?
2020-09-04 10:40:34 -07:00
Leonardo de Moura
555a3f0dcf
feat: new and improved mkAuxDefinition
2020-09-03 17:37:06 -07:00
Leonardo de Moura
f34fd3e6b4
refactor: move Closure.lean to Meta
...
We will need to improve the support for let-decls. We will use
the new `trackZeta`.
2020-09-03 11:54:08 -07:00
Leonardo de Moura
ad774ae397
feat: support for tracking which let-decls have been zeta expanded
2020-09-03 11:32:46 -07:00
Leonardo de Moura
907a202961
feat: expand in command macro
2020-09-02 10:04:58 -07:00
Leonardo de Moura
988bb09aaf
feat: new inductive command syntax
...
cc @Kha
2020-09-02 09:41:52 -07:00
Sebastian Ullrich
75b2dc1baf
refactor: simplify ppModule using new module parser
2020-08-31 15:44:58 +02:00
Leonardo de Moura
2f4340f63c
feat: refine refine tactic
...
Now `refine stx` reports an error when there are natural unassigned
metavariables after we elaborate syntax `stx`. The idea is that only
synthetic holes `?<hole-name>` become new goals.
The tactic `refine! stx` implements the Lean3 behavior.
2020-08-30 16:14:38 -07:00
Leonardo de Moura
6f0e9452b2
chore: remove begin ... end syntax
...
We should use `by { ... }` from now on.
cc @Kha
2020-08-30 14:15:33 -07:00
Leonardo de Moura
b74741b741
chore: "begin ... end" ==> "by { ... }"
...
cc @Kha
2020-08-30 14:01:27 -07:00
Leonardo de Moura
052e830db7
feat: add have, show, let, let!, and suffices tactic macros
...
They are all simple macros based on: `refine` + syntheticHoles
2020-08-30 08:26:15 -07:00
Leonardo de Moura
2eb330e36a
feat: improve clear tactic
2020-08-29 20:19:33 -07:00
Leonardo de Moura
9e075e39a5
feat: eval new intro "macro"
...
It is as powerful as the new `fun` term
2020-08-29 17:09:21 -07:00
Leonardo de Moura
3d3238c7fe
fix: typo at introNCoreAux
2020-08-29 17:00:59 -07:00
Leonardo de Moura
99f3296828
refactor: simplify Util/Trace.lean
2020-08-28 17:36:44 -07:00
Leonardo de Moura
e0d39e6a7d
feat: use whnf at subst
2020-08-28 15:56:28 -07:00
Leonardo de Moura
2287c7e7b3
feat: elaborate #print axioms command
2020-08-28 13:08:42 -07:00
Leonardo de Moura
50470c328f
test: nativeRefl! abuse example
2020-08-28 12:09:25 -07:00
Sebastian Ullrich
110ae4b571
feat: replace OS-specific stream redirection with pure-Lean Stream redirection
...
This avoids the temporary files workaround on macOS and Windows, and makes sure
we can process a `#eval` command and write messages to stdout at the same time.
2020-08-28 10:04:32 -07:00
Leonardo de Moura
54f95421c8
test: Lean2 obtain is just a macro
2020-08-28 09:37:29 -07:00
Leonardo de Moura
62177069fd
fix: induction tactic
2020-08-28 09:18:22 -07:00
Leonardo de Moura
0b7a7f7b90
feat: better support for _ in match tactic
2020-08-27 18:18:49 -07:00
Leonardo de Moura
76bda91ff8
feat: add evalMatch for tactics
2020-08-27 18:05:06 -07:00
Leonardo de Moura
4934a2d522
chore: remove workaround
2020-08-26 16:24:20 -07:00
Leonardo de Moura
5a7bf86a42
test: add test for buggy compiler step
...
Bug was fixed at da928f8c0
2020-08-26 08:34:35 -07:00
Leonardo de Moura
321719b300
feat: add MonadFinally
2020-08-25 17:58:35 -07:00
Leonardo de Moura
7888919aa9
test: MonadControl
2020-08-25 13:54:41 -07:00
Leonardo de Moura
b095f0652a
fix: tryLiftAndCoe
2020-08-25 13:54:41 -07:00
Leonardo de Moura
e5b7daf9c2
refactor: make AppBuilder methods polymorphic
2020-08-24 18:23:34 -07:00
Leonardo de Moura
14f973d5a0
chore: fix tests
2020-08-24 17:59:11 -07:00
Leonardo de Moura
fab100abb4
chore: fix tests
2020-08-24 12:17:47 -07:00
