Sebastian Ullrich
8a5febf130
chore: CI: fix release job
2022-03-23 19:33:25 +01:00
Leonardo de Moura
be7c71d1c8
chore: update date
2022-03-23 07:44:15 -07:00
Leonardo de Moura
e0aa9fb290
chore: fix typo
2022-03-23 07:39:46 -07:00
Leonardo de Moura
170b911a6f
doc: expand deBruijn
2022-03-22 19:35:58 -07:00
Leonardo de Moura
20fb3e470d
doc: add dependent de Bruijn indices
...
TODO: explain example.
2022-03-22 19:11:06 -07:00
Leonardo de Moura
b2a1b88a4e
doc: a certified type checker
2022-03-22 19:01:26 -07:00
Leonardo de Moura
a23fcb6033
chore: use github link until we generate the proper webpage using Alectryon
2022-03-22 18:34:40 -07:00
Leonardo de Moura
028e3561e2
fix: link
2022-03-22 18:07:04 -07:00
Leonardo de Moura
265803f7ac
doc: fix links
2022-03-22 16:52:08 -07:00
Leonardo de Moura
e06893d1f2
doc: proper TPIL link
2022-03-22 16:37:16 -07:00
Leonardo de Moura
973b76a6e2
doc: add Examples section
2022-03-22 16:35:14 -07:00
Leonardo de Moura
412bc14fbe
doc: add well-typed interpreter as an example
2022-03-22 16:32:41 -07:00
Leonardo de Moura
5ae125262b
chore: remove C++ coding style from manual
2022-03-22 15:54:51 -07:00
Leonardo de Moura
2e9adf0e04
chore: remove broken documentation
2022-03-22 15:52:13 -07:00
Leonardo de Moura
9d32d7bcf5
test: for issue #1062
...
closes #1062
2022-03-22 14:14:28 -07:00
Leonardo de Moura
2f67140603
fix: incorrect uses of getMVarType'
2022-03-22 14:11:29 -07:00
Leonardo de Moura
6007147d71
fix: allow universes to be postponed further
...
closes #1058
2022-03-22 13:57:58 -07:00
Leonardo de Moura
f3b181b972
chore: comment withoutPostponingUniverseConstraints
2022-03-22 13:57:58 -07:00
Mario Carneiro
c29da66c5a
fix: annotate binders in intro for hover / go to def
2022-03-22 12:10:51 +00:00
Sebastian Ullrich
3818ea8333
chore: CI: document previous workaround
2022-03-22 12:25:59 +01:00
Sebastian Ullrich
c758d442dc
chore: CI: try using the correct C++ compiler for tests on Windows
2022-03-22 12:22:23 +01:00
Sebastian Ullrich
bba0baf92c
chore: CI: I'm sure they work fine
2022-03-22 12:22:23 +01:00
Sebastian Ullrich
82049c519c
chore: CI: fix MinGW library root
2022-03-22 12:22:23 +01:00
Sebastian Ullrich
00aeaed544
chore: CI: fix manual build
2022-03-22 09:36:52 +01:00
Sebastian Ullrich
c4d3c74837
feat: accept multiple patterns after matches
2022-03-21 17:59:02 +01:00
Sebastian Ullrich
cb93590f0b
chore: update stage0
2022-03-21 17:47:03 +01:00
Sebastian Ullrich
faedfbe651
fix: antiquotation splices early in bootstrapping
2022-03-21 17:44:15 +01:00
Leonardo de Moura
3d9e587862
fix: check type mismatch at dependent pattern matching compiler
...
see issue #1057
2022-03-21 09:28:02 -07:00
Leonardo de Moura
9944feb095
test: use [reducible]
2022-03-21 07:39:44 -07:00
Sebastian Ullrich
89a3f6d623
chore: update Lake
2022-03-21 14:50:54 +01:00
Sebastian Ullrich
1a5822a3e2
chore: update Lake
2022-03-21 14:02:36 +01:00
Leonardo de Moura
3a75cf1920
test: nested inductives
2022-03-21 05:57:02 -07:00
Leonardo de Moura
cba204e3cb
chore: update stage0
2022-03-20 18:47:28 -07:00
Leonardo de Moura
321d6b0e67
feat: support for user-defined simp attributes in the simp tactic.
...
See `RELEASES.md`
TODO: make sure `-thm` also removes `thm` from user-defined simp attributes.
2022-03-20 18:45:57 -07:00
Leonardo de Moura
a2690d5278
feat: improve #eval command
2022-03-20 15:18:47 -07:00
Leonardo de Moura
7b1091770c
test: Repr for HList
2022-03-20 15:05:34 -07:00
Leonardo de Moura
6d926c7989
feat: macro expand match alternatives
...
see #371
This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
| S (s : String)
| I (i : Int)
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a => toString a
| S a => toString a
```
2022-03-20 14:20:13 -07:00
Leonardo de Moura
51ee6fe4f1
chore: fix test
2022-03-20 13:27:19 -07:00
Leonardo de Moura
476bcee8ba
chore: update stage0
2022-03-20 13:25:03 -07:00
Leonardo de Moura
8f4d58893f
feat: update match parser
...
Support for
```
def fib (x : Nat) : Nat :=
match x with
| 0 | 1 => 1
| x+2 => fib (x+1) + fib x
```
TODO: expand `matchAlts`
2022-03-20 13:22:39 -07:00
Leonardo de Moura
87bb299f08
feat: add Iterator.atEnd
2022-03-20 11:40:46 -07:00
Leonardo de Moura
4f9dcd55ce
chore: update stage0
2022-03-20 10:59:21 -07:00
Leonardo de Moura
3862e7867b
refactor: make String.Pos opaque
...
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`
closes #410
2022-03-20 10:47:13 -07:00
Jakob von Raumer
a91f92c11e
feat: allow constants to be type classes
...
There no reason against constants to be type classes so it is just the check in `addClass` that is needed to be modified.
Closes #1054
2022-03-20 08:03:34 -07:00
Leonardo de Moura
6e94801c00
chore: update stage0
2022-03-19 16:55:26 -07:00
Leonardo de Moura
1b357db3b0
fix: nasty bug at findDeclarationRangesCore?
...
We must search the environment extension first, and then the builtin
table. Otherwise, the builtin declarations do not change when we
modify the files.
closes #1021
2022-03-19 16:53:22 -07:00
Leonardo de Moura
ed7c8904a9
fix: propagate local and scope modifiers at elab_rules
...
closes #1039
2022-03-19 16:08:06 -07:00
Leonardo de Moura
82cd5c8eef
chore: cleanup
2022-03-19 15:52:04 -07:00
E.W.Ayers
da68f629f9
style: Apply.lean
...
Apply Leo's review requests.
2022-03-19 15:51:40 -07:00
E.W.Ayers
d954706fcf
feat: ApplyNewGoals config for apply
...
Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.
Closes #1045
2022-03-19 15:51:40 -07:00
