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
casavaca
bf4ba1583d
feat: add simp theorem for List, (as.map f).length = as.length
2022-03-19 11:35:21 -07:00
Leonardo de Moura
72b6f4d528
chore: avoid unnecessary h :s
2022-03-19 11:21:37 -07:00
Leonardo de Moura
f29319647f
chore: update stage0
2022-03-19 11:16:24 -07:00
Leonardo de Moura
4f318d3304
test: use dot notation in the example
2022-03-19 10:39:58 -07:00
Leonardo de Moura
d1eb180aae
test: add non mutually recursive version
2022-03-19 10:38:39 -07:00
Leonardo de Moura
bdb2e9597a
chore: naming convention
2022-03-19 10:20:42 -07:00
Leonardo de Moura
6c8322d20a
test: use builtin Char.isDigit and Char.toNat
2022-03-19 10:18:34 -07:00
Leonardo de Moura
a8ddb56e0e
chore: cleanup David's example
2022-03-19 10:13:27 -07:00
Leonardo de Moura
c95d5f25a3
feat: convert ites into dites in the WF module
...
Motivation: the condition is often used in termination proofs.
2022-03-19 10:11:50 -07:00
Leonardo de Moura
9fed5bda7d
chore: remove workarounds
2022-03-19 09:44:57 -07:00
Leonardo de Moura
544421faf5
chore: update stage0
2022-03-19 09:43:57 -07:00
