Leonardo de Moura
c9a9dbcede
chore: update stage0
2020-11-25 11:02:26 -08:00
Leonardo de Moura
2c19eb08cb
feat: add erewrite tactic
...
This commits also change `rewrite`. It was behaving like Lean 3
`erewrite` which is too expensive.
2020-11-25 11:02:25 -08:00
Leonardo de Moura
9023e93b3e
refactor: move Array.set to Prelude
2020-11-25 11:02:25 -08:00
Sebastian Ullrich
bbe3d51c44
chore: Nix: hide some Nix warnings in lean-dev
...
/cc @javra
2020-11-25 18:37:33 +01:00
Leonardo de Moura
551d4607ae
chore: update stage0
2020-11-25 09:26:33 -08:00
Leonardo de Moura
e3fb7010f1
chore: fix tests
2020-11-25 09:25:45 -08:00
Leonardo de Moura
d6f778bec4
refactor: arbitrary without explicit arguments
...
@Kha I was tired of writing `arbitrary _` :)
There 0 places in the stdlib where the type needs to be provided.
If in the future we need to specify the type we can use
`arbitrary (α := <type>)`
2020-11-25 09:07:38 -08:00
Leonardo de Moura
5c20467600
chore: update stage0
2020-11-25 08:32:22 -08:00
Leonardo de Moura
3b75a56160
chore: prepare to make arbitrary argument implicit
2020-11-25 08:30:03 -08:00
Leonardo de Moura
6976f4501e
chore: cleanup
2020-11-25 08:19:17 -08:00
Sebastian Ullrich
de20b14366
feat: delaborate basic do
...
/cc @leodemoura
2020-11-25 16:00:56 +01:00
Sebastian Ullrich
e2ff1c2b7e
chore: update stage0
2020-11-25 12:39:26 +01:00
Sebastian Ullrich
192ee5372a
fix: Nix: update-stage0
2020-11-25 12:13:22 +01:00
Sebastian Ullrich
375e6232e0
chore: introduce doSeqItem kind
2020-11-25 12:10:49 +01:00
Sebastian Ullrich
bd7bb6f5b5
fix: do formatting
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
b22e035b6f
fix: pretty print empty matchers as nomatch
...
/cc @leodemoura
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
cf9a2ae6af
feat: formatter: preserve comments
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
871cd105dc
feat: Syntax.updateLeading: also choose "nicer" splits
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
727816e7fd
test: bring back Reformat.lean on abbreviated copy of Prelude.lean
...
/cc @leodemoura
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
33c1e5ed9e
fix: formatter: ignore all but one choice node
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
6126fd6388
chore: improve pretty printer traces, avoid recursion
2020-11-25 11:30:24 +01:00
Sebastian Ullrich
45a315d273
doc: Nix: seems to work fine on macOS
2020-11-25 09:48:50 +01:00
Leonardo de Moura
46dfe7b911
doc: expand tactics.md
2020-11-24 16:56:09 -08:00
Leonardo de Moura
1aeb88cee5
feat: add where example in proofs
2020-11-24 16:30:28 -08:00
Leonardo de Moura
1cb7cb3ef6
feat: add exists tactic
2020-11-24 16:17:43 -08:00
Leonardo de Moura
22629b3c66
feat: add headBetaMVarType
2020-11-24 16:17:27 -08:00
Leonardo de Moura
36eb03c601
chore: cleanup Check.lean
2020-11-24 16:13:52 -08:00
Leonardo de Moura
b72a3c69b6
fix: ambiguity at induction/cases
...
See efc3a320fe
2020-11-24 14:59:12 -08:00
Leonardo de Moura
ec1e684281
chore: update stage0
2020-11-24 14:49:38 -08:00
Leonardo de Moura
efc3a320fe
chore: prepare to fix ambiguity at induction/cases notation
...
@Kha I was writing the following example
```
...
induction as
| nil => cases h -- `h` is an empty type
| cons b bs ih => cases h
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| tail a b bs h1 => ...
```
The current `syntax` assumes the `| cons b bs ih => ...` alternative
is part of the first `cases h`. Forcing the `|` to occur in a column
>= of the corresponding `cases` is not a nice solution since it would
preven us from writing the second `cases` as I wrote it above.
That is we would have to write
```
induction as
| nil => cases h -- `h` is an empty type
| cons b bs ih =>
cases h
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| tail a b bs h1 => ...
```
or
```
induction as
| nil => cases h -- `h` is an empty type
| cons b bs ih => cases h
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| tail a b bs h1 => ...
```
I think the best solution is to use `with` when we have explicit
alternatives with `|`. The new syntax is similar to `match ... with | ...`
That is, we would write
```
...
induction as with
| nil => cases h
| cons b bs ih => cases h with
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| tail a b bs h1 => ...
```
2020-11-24 14:33:19 -08:00
Leonardo de Moura
5585f9823f
chore: cleaner structure/class syntax
...
@Kha I implemented the syntax for structure/class that we discussed this morning.
It is much cleaner. See new tests at `struct2.lean`.
I updated the documentation to use it.
2020-11-24 13:07:43 -08:00
Leonardo de Moura
cf0bb173ad
fix: highlight.js
2020-11-24 12:53:54 -08:00
Leonardo de Moura
495b6a92e9
feat: add IO.sleep ms
...
I am going to use it in the documentation: `Task` examples.
2020-11-24 11:27:04 -08:00
Leonardo de Moura
fa04f46d55
doc: simplify begin..end macro
...
The method `getRef` returns the whole term being expanded.
@Kha The method was originially added for reporting error messages.
So, the name is counterintuitive.
2020-11-24 11:06:49 -08:00
Leonardo de Moura
3eaa4518a0
test: dependent pattern matching
2020-11-24 11:06:49 -08:00
Sebastian Ullrich
2c64441910
chore: Nix: disable dirty Git tree warning & fix lean4-diff-test-file
...
/cc @leodemoura
Note that you will have to restart Emacs and the "Lean shell" around it for the changes to take effect
2020-11-24 20:05:24 +01:00
Leonardo de Moura
8f1ad0411d
fix: fixes #220 and #223
2020-11-24 10:18:02 -08:00
Leonardo de Moura
5c39cd5120
chore: cleanup
2020-11-24 10:18:02 -08:00
Leonardo de Moura
ecfe590268
refactor: split Match.lean
2020-11-24 10:18:02 -08:00
Sebastian Ullrich
a180a4c080
fix: Nix: don't try to push PRs
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
6be438d7b1
doc: Nix: more notes
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
e9bb7c1175
fix: CI: macOS job
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
6be577b634
fix: CI: Linux release job
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
3e8693fac8
fix: Nix: provide .#lean-package etc. from Lean package
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
4f89cbf9b9
doc: Nix: explain some warnings
...
/cc @leodemoura @javra
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
bc0010b84c
fix: Nix: Lean module ccache
...
Now I remember again why I did that the way I did it
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
d61cb698aa
chore: hide matrix parameters in CI job names
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
1b302f328f
doc: fix Bash comment highlighting
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
e0d9bc2f9b
chore: Nix: simplify flake.nix after all and fix shell.nix
2020-11-24 19:16:27 +01:00
Sebastian Ullrich
a5ad46f7be
feat: Nix: mdbook
2020-11-24 19:16:27 +01:00
