Sebastian Ullrich
8175003707
doc: update links to elan
2021-04-17 16:33:23 +02:00
Leonardo de Moura
46e02bcdcc
chore: fix stdlib
2021-04-16 21:59:44 -07:00
Leonardo de Moura
bb5a46cd61
chore: update stage0
2021-04-16 21:50:02 -07:00
Leonardo de Moura
157ef80c5a
feat: match auto generalization
2021-04-16 21:48:38 -07:00
Leonardo de Moura
aaa072cf21
feat: add withNewBinderInfos
2021-04-16 09:59:40 -07:00
Leonardo de Moura
3bd34182ee
chore: generalizing skeleton
2021-04-16 09:51:12 -07:00
Daniel Fabian
cb18af6184
feat: add withLocalDecls and withLocalDeclsD
...
They are array versions of `withLocalDecl` and `withLocalDeclD`, respectively. They are useful when you need to create variables dynamically.
2021-04-16 07:54:04 -07:00
Leonardo de Moura
555b978d67
refactor: add GeneralizeVars.lean
...
Helper methods for performing auto generalization.
2021-04-15 21:37:48 -07:00
Leonardo de Moura
2667744092
fix: panic message
2021-04-15 18:25:19 -07:00
Leonardo de Moura
1c23d68c6a
feat: add (generalizing := true/false) optional attribute to match
2021-04-15 17:04:25 -07:00
Leonardo de Moura
47bb80a277
chore: update stage0
2021-04-15 12:40:45 -07:00
Leonardo de Moura
f6651605d0
chore: remove unnecessary modification, fun syntax is not a binder
2021-04-15 12:38:48 -07:00
Leonardo de Moura
747bb486b8
chore: update stage0
2021-04-15 12:34:44 -07:00
Leonardo de Moura
36a4f337e9
fix: fixes #247
2021-04-15 12:33:45 -07:00
Leonardo de Moura
dbc84c502c
chore: make sure we don't lift methods over binders
2021-04-15 12:06:46 -07:00
Sebastian Ullrich
91169f9987
doc: quickstart: formatting, again
2021-04-15 19:08:56 +02:00
Paul Brinkmeier
c1623add68
doc: add note about staging flake.nix ( #411 )
...
If you don't make flake.nix visible to Git, nix build etc. won't work. Add a command that adds the file to the Index and a note explaining why.
2021-04-15 18:45:22 +02:00
Sebastian Ullrich
32fd82efc2
fix: link lean statically against GMP again
2021-04-14 20:37:07 +02:00
Leonardo de Moura
0a1923b820
chore: update faq with "help wanted" link
2021-04-14 07:30:09 -07:00
Leonardo de Moura
c1f45ecd48
fix: fixes #394
...
The bug was due to the auto-generalization feature.
2021-04-13 19:14:57 -07:00
Leonardo de Moura
327eb1a96d
fix: ensure ill-formed if do-statements do not trigger non termination
2021-04-13 15:51:20 -07:00
Leonardo de Moura
2384826933
chore: add loop prenvention code at do-expander
2021-04-13 15:46:47 -07:00
Leonardo de Moura
1a2a089c28
chore: comment
2021-04-13 10:34:19 -07:00
Leonardo de Moura
adda3a9e02
fix: improve structural recursion
2021-04-13 10:31:43 -07:00
Sebastian Ullrich
435431ca7e
feat: hide elaboration errors from partial syntax trees by default
2021-04-13 19:24:35 +02:00
Leonardo de Moura
292bab5a11
fix: loop due to error recovery
2021-04-13 08:12:39 -07:00
Leonardo de Moura
59d7008f24
chore: cleanup
2021-04-13 08:12:14 -07:00
Leonardo de Moura
bf4b9b0ccd
fix: use noImplicitLambda% when defining tactic macros such as have, let, etc
...
Thus, we don't change the expected type when using them.
2021-04-12 23:01:47 -07:00
Leonardo de Moura
ecad25e08f
chore: update stage0
2021-04-12 22:56:56 -07:00
Leonardo de Moura
2f37d7e290
feat: elaborate noImplicitLambda% notation
2021-04-12 22:55:17 -07:00
Leonardo de Moura
635a320455
chore: ignore mdata at intros
2021-04-12 22:38:15 -07:00
Leonardo de Moura
4b56ca066d
chore: update stage0
2021-04-12 22:35:09 -07:00
Leonardo de Moura
abf78e162c
feat: add notation for disabling implicit lambda feature
...
This notation will be useful for writing macros where
implicit lambdas are not desired.
2021-04-12 22:33:23 -07:00
Leonardo de Moura
d2910337af
test: completion
2021-04-12 22:32:27 -07:00
Leonardo de Moura
40a42128be
fix: auto completion improvements
2021-04-12 19:22:56 -07:00
Daniel Selsam
d35091da56
feat: parser alias for 'declVal'
2021-04-12 16:59:54 -07:00
Leonardo de Moura
217c0391bb
chore: example
2021-04-12 16:56:10 -07:00
Sebastian Ullrich
92810602d0
fix: server: do not stop processing after error (except for header error)
2021-04-12 22:41:10 +02:00
Leonardo de Moura
565ca259b1
fix: issue raised by Andrew
2021-04-12 10:51:44 -07:00
Sebastian Ullrich
1e61b7db89
fix: partial syntax tree panic
...
Fixes #391
2021-04-12 18:33:39 +02:00
Leonardo de Moura
5fc1a86274
chore: indentation
2021-04-11 22:00:21 -07:00
Leonardo de Moura
7950907dac
chore: update stage0
2021-04-11 21:49:23 -07:00
Leonardo de Moura
83b83f51e9
fix: resolveProvider?
...
Recent bug fixes exposed a problem here.
The field `resolveProvider?` has a `?`, but is not an `Option`
type. The `ToJson` makes this assumption and uses the auxiliary
function `opt`. The bugs fixed today were masjing this problem.
2021-04-11 21:45:59 -07:00
Leonardo de Moura
f55561008c
fix: fixes #386
2021-04-11 20:57:39 -07:00
Leonardo de Moura
5d4c96e5d6
test: expand test for 389
2021-04-11 20:55:33 -07:00
Leonardo de Moura
7ae279d04f
fix: missing commitWhenSome? at tryPureCoe?
...
fixes #389
2021-04-11 19:28:34 -07:00
Leonardo de Moura
47735d6706
chore: remove dead function
...
Moreover, it is incorect to save/restore the metavariable context
without saving/restoring `Term.State` fields contain metavariables
being rolled back.
2021-04-11 19:17:55 -07:00
Leonardo de Moura
e5d8158cef
chore: update stage0
2021-04-11 19:12:56 -07:00
Leonardo de Moura
23f49c35fc
refactor: MonadBacktrack for TacticM
2021-04-11 19:10:41 -07:00
Leonardo de Moura
484a3a4e7c
fix: should only cache inferred type when there are no metavars
2021-04-11 19:10:41 -07:00
