Leonardo de Moura
|
5c101d056a
|
doc: update contribution guidelines
|
2021-05-13 15:17:11 -07:00 |
|
Leonardo de Moura
|
ea45d3bd40
|
fix: fixes #457
|
2021-05-12 20:45:54 -07:00 |
|
Leonardo de Moura
|
4db3ccaddb
|
feat: type ascription should disable implicit lambdas
|
2021-05-12 19:29:36 -07:00 |
|
Daniel Fabian
|
0eaa36b38d
|
Update CONTRIBUTING.md
|
2021-05-12 07:06:18 -07:00 |
|
Sebastian Ullrich
|
8ae726203d
|
fix: plainGoal: consider original positions only when deciding whether a tactic is a combinator
|
2021-05-12 10:51:42 +02:00 |
|
Leonardo de Moura
|
c9db8619f1
|
fix: fixes #456
|
2021-05-11 21:07:21 -07:00 |
|
Sebastian Ullrich
|
1e6dadfa52
|
fix: documentHighlight on partial input
Fixes #455
|
2021-05-11 17:03:18 +02:00 |
|
Xavier Noria
|
d35f46d4ba
|
doc: fix spelling of GitHub in the FAQ (#454)
|
2021-05-11 09:15:07 +02:00 |
|
Leonardo de Moura
|
ad88a1f406
|
chore: update stage0
|
2021-05-10 20:09:14 -07:00 |
|
Leonardo de Moura
|
ad45c18503
|
fix: fixes #448
|
2021-05-10 20:07:28 -07:00 |
|
Leonardo de Moura
|
b52edf1259
|
fix: fixes #452
The new syntax is similar to `matchAlts` and uses `colGe`.
The first `|` is not optional anymore.
|
2021-05-10 17:28:10 -07:00 |
|
Leonardo de Moura
|
0a57cbd7d3
|
chore: update stage0
|
2021-05-10 17:06:23 -07:00 |
|
Leonardo de Moura
|
7d39a0d56c
|
chore: prepare to change first syntax
|
2021-05-10 17:05:31 -07:00 |
|
Leonardo de Moura
|
0e1f645b07
|
fix: fixes #450
|
2021-05-10 13:55:06 -07:00 |
|
Leonardo de Moura
|
e49dfccc2a
|
chore: remove dead variable
|
2021-05-10 13:41:55 -07:00 |
|
Leonardo de Moura
|
2a676b6dfb
|
fix: fixes #449
|
2021-05-10 13:10:59 -07:00 |
|
Leonardo de Moura
|
89373bd64f
|
fix: fixes #447
|
2021-05-08 19:04:12 -07:00 |
|
Leonardo de Moura
|
4675817a9e
|
fix: projection of string literals
|
2021-05-07 14:38:21 -07:00 |
|
Leonardo de Moura
|
5fcd08326f
|
fix: bug at reduceRec
|
2021-05-07 14:21:37 -07:00 |
|
Sebastian Ullrich
|
7b128b308b
|
fix: leak in lean_mk_array
|
2021-05-07 18:20:32 +02:00 |
|
Sebastian Ullrich
|
05b12e2b61
|
chore: undo workaround
|
2021-05-07 16:09:42 +02:00 |
|
Sebastian Ullrich
|
0583970ad8
|
chore: update stage0
|
2021-05-07 16:09:02 +02:00 |
|
Sebastian Ullrich
|
088774536e
|
fix: syntax match: do not discard other patterns after splices
|
2021-05-07 16:08:10 +02:00 |
|
Sebastian Ullrich
|
6f9b80d91c
|
fix: parenthesizer: avoid panic on partial syntax trees
Fixes #446
|
2021-05-07 09:42:14 +02:00 |
|
Leonardo de Moura
|
475f5fecaa
|
feat: improve error recovery at Tactic.elabTerm
|
2021-05-06 20:44:36 -07:00 |
|
Leonardo de Moura
|
8e81f03e3a
|
chore: adjust stdlib to recent changes
|
2021-05-06 15:43:56 -07:00 |
|
Leonardo de Moura
|
7a7ba648d5
|
chore: update stage0
|
2021-05-06 15:40:07 -07:00 |
|
Leonardo de Moura
|
7fc6607611
|
feat: have ... := ... syntax closer to let
|
2021-05-06 15:38:57 -07:00 |
|
Leonardo de Moura
|
73b7a754ee
|
fix: let_fun with patterns
|
2021-05-06 15:11:22 -07:00 |
|
Leonardo de Moura
|
48bffedc74
|
fix: unresolved holes in the exact tactic, backtracking issues
This commit also adds the `throwAbortTactic` for throwing "silent"
exceptions in `TacticM`.
|
2021-05-06 13:44:01 -07:00 |
|
Sebastian Ullrich
|
99864bbb31
|
chore: reintroduce ∅ as regular notation
|
2021-05-06 22:41:23 +02:00 |
|
Sebastian Ullrich
|
e1d3a71d6f
|
chore: update stage0
|
2021-05-06 22:16:45 +02:00 |
|
Sebastian Ullrich
|
baa2781eb0
|
chore: remove built-in emptyC syntax/elaborator
|
2021-05-06 22:07:03 +02:00 |
|
Sebastian Ullrich
|
a85d0672fe
|
chore: Nix CI: fall back to building locally if remote cache doesn't work
|
2021-05-06 22:07:03 +02:00 |
|
Sebastian Ullrich
|
9ed8db4bc3
|
feat: add constructor tactic
|
2021-05-06 10:40:56 -07:00 |
|
Бакиновский Максим
|
c96cb78970
|
doc: "enumerated types" section markdown fix
|
2021-05-06 17:04:51 +02:00 |
|
Sebastian Ullrich
|
e6132d37a5
|
fix: induction/cases: accept wildcard alternative even if some (but not all) cases have been excluded
|
2021-05-06 14:28:00 +02:00 |
|
Leonardo de Moura
|
c4e3b36d56
|
test: for issue #439
closes #439
|
2021-05-05 11:13:23 -07:00 |
|
Leonardo de Moura
|
7eec7b7842
|
fix: only use .( ... ) when delaborating patterns
|
2021-05-05 11:12:44 -07:00 |
|
Leonardo de Moura
|
6fd65d61d2
|
chore: update stage0
|
2021-05-05 10:59:56 -07:00 |
|
Leonardo de Moura
|
b4a7d28cff
|
fix: inconsistent inaccessible annotations
|
2021-05-05 10:45:38 -07:00 |
|
Leonardo de Moura
|
660c49840f
|
fix: another instance of the binder cache issue
See issue #439
|
2021-05-05 10:45:38 -07:00 |
|
Sebastian Ullrich
|
6303c134a9
|
feat: add term info at resolveId?
|
2021-05-05 18:54:47 +02:00 |
|
Sebastian Ullrich
|
66c0f6ae9d
|
fix: goal state at induction/cases e with
|
2021-05-05 15:27:40 +02:00 |
|
Sebastian Ullrich
|
84d3896ea7
|
chore: fix comment
|
2021-05-05 15:08:30 +02:00 |
|
Sebastian Ullrich
|
456264bf31
|
chore: pretty printer: tolerate missing better
|
2021-05-05 14:46:05 +02:00 |
|
Sebastian Ullrich
|
76c66fc4d4
|
fix: error message
|
2021-05-05 14:45:50 +02:00 |
|
Leonardo de Moura
|
a43dca0b9f
|
fix: add basic support for accessing the field of a section variable in the notation prechecker
see #435
|
2021-05-04 22:41:25 -07:00 |
|
Leonardo de Moura
|
3d829c825c
|
fix: Info nodes for overloaded notation/declarations
See new test to understand the problem that has been fixed.
|
2021-05-04 22:07:21 -07:00 |
|
Leonardo de Moura
|
ed1eee201a
|
fix: avoid "failed to evaluate" error when extension has sorry
See updated test output.
|
2021-05-04 20:57:53 -07:00 |
|