Sebastian Ullrich
d0fb48b4e4
fix: use builtin code action for "try this"
2024-02-20 12:48:19 +01:00
Sebastian Ullrich
79a9f6759a
chore: update stage0
2024-02-20 12:48:19 +01:00
Sebastian Ullrich
f1a3169424
fix: [builtin_code_action_provider]
2024-02-20 12:48:19 +01:00
Scott Morrison
4a7c1ea439
chore: upstream simp?
2024-02-20 12:48:19 +01:00
Scott Morrison
15cbcae7b2
chore: typo ( #3415 )
2024-02-20 10:40:59 +00:00
Scott Morrison
ea665de453
chore: CI checks for copyright headers ( #3412 )
...
Hopefully this will fail until #3411 is merged.
2024-02-20 07:02:50 +00:00
Scott Morrison
8b8e001794
chore: add missing copyright headers ( #3411 )
2024-02-20 01:49:55 +00:00
Scott Morrison
35e374350c
chore: upstream norm_cast tactic ( #3322 )
...
This is a quite substantial tactic.
It also includes the infamour `NatCast` typeclass (which I've equipped
with a module-doc). I wasn't at all sure where that should live, so it
is currently randomly in `Lean/Elan/Tactic/NatCast.lean`: presumably if
we're doing this it will go somewhere in `Init`.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
2024-02-19 17:49:17 -08:00
Leonardo de Moura
9e27e92eea
chore: set literal notation ( #3348 )
...
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
2024-02-19 23:22:36 +00:00
Leonardo de Moura
489f2da711
feat: add simproc for BitVec.signExtend ( #3409 )
2024-02-19 15:15:37 -08:00
Leonardo de Moura
75d7bc0ef1
chore: disable test to fix build failure on Windows ( #3410 )
2024-02-19 15:15:26 -08:00
Leonardo de Moura
5d9552d66c
feat: simprocs for BitVec ( #3407 )
2024-02-19 14:01:00 -08:00
Leonardo de Moura
067913bc36
chore: remove sorry
2024-02-19 13:01:44 -08:00
Leonardo de Moura
c23a35c472
chore: quick temporary fix
2024-02-19 12:53:25 -08:00
Leonardo de Moura
f64d14ea54
chore: update stage0
2024-02-19 12:47:04 -08:00
Leonardo de Moura
90b5a0011d
feat: assume function application arguments occurring in local simp theorems have been annotated with no_index ( #3406 )
...
closes #2670
2024-02-19 12:43:34 -08:00
Scott Morrison
ca941249b9
chore: upstream Std.BitVec.* ( #3400 )
...
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
2024-02-19 12:43:34 -08:00
Sebastian Ullrich
94a9ab45ff
chore: Nix CI: stop pushing to cachix ( #3402 )
2024-02-19 16:41:20 +00:00
Joe Hendrix
e2b3b34d14
feat: introduce native functions for Int.ediv / Int.emod ( #3376 )
...
These still need tests, but I thought I'd upstream so I can use
benchmarking and check for build errors.
2024-02-19 15:04:51 +00:00
Sebastian Ullrich
204b408df7
chore: remove noisy root code owners
2024-02-19 17:30:21 +01:00
Lean stage0 autoupdater
7545b85512
chore: update stage0
2024-02-19 15:51:18 +00:00
Sebastian Ullrich
1d66c32d5f
fix: weaken builtin widget collision check
2024-02-19 15:45:01 +00:00
Scott Morrison
7f08975176
chore: upstream simpa ( #3396 )
2024-02-19 13:37:34 +00:00
Sebastian Ullrich
0e0ed9ccaf
fix: broken trace tree on elab runtime exception ( #3371 )
2024-02-19 11:15:23 +00:00
Sebastian Ullrich
59bf220934
chore: update stage0
2024-02-19 12:37:19 +01:00
Sebastian Ullrich
032a2ecaa1
chore: update builtin_widget_module registration code
2024-02-19 12:33:23 +01:00
Joachim Breitner
da24708ba5
refactor: use isAppOfArity ( #3394 )
2024-02-19 09:24:11 +00:00
Scott Morrison
16757bb256
chore: upstream Std.Data.Fin.Iterate ( #3392 )
2024-02-19 04:29:45 +00:00
Scott Morrison
3f548edcd7
chore: upstream (most of) Std.Data.Nat.Lemmas ( #3391 )
...
When updating Std, be careful that not every lemma has been upstreamed,
so we need to be careful to only delete things that have already been
declared.
2024-02-19 03:47:49 +00:00
Scott Morrison
8758c0adf5
chore: upstream Std.Data.Bool ( #3389 )
2024-02-19 02:44:07 +00:00
Scott Morrison
b41499cec1
chore: upstream Std.Data.Fin.Basic ( #3390 )
2024-02-19 02:16:17 +00:00
Scott Morrison
88deb34ddb
chore: upstream omega ( #3367 )
...
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
2024-02-19 00:19:55 +00:00
Sebastian Ullrich
5e5bdfba1a
fix: savePanelWidgetInfo on @[builtin_widget_module] ( #3329 )
2024-02-18 22:47:30 +00:00
Henrik Böving
23e49eb519
perf: add prelude to all Lean modules
2024-02-18 14:55:17 -08:00
Leonardo de Moura
5ce20ba160
chore: add link to issue
2024-02-18 14:19:01 -08:00
Leonardo de Moura
aa42fc07d3
test: for issue #2843
...
closes #2843
2024-02-18 14:14:55 -08:00
Leonardo de Moura
bc74e6eb38
chore: update RELEASES.md
2024-02-18 14:14:55 -08:00
Leonardo de Moura
52f1fcc498
chore: remove workaround
2024-02-18 14:14:55 -08:00
Leonardo de Moura
a6cdc333d5
chore: fix tests
2024-02-18 14:14:55 -08:00
Leonardo de Moura
58ed6b9630
chore: update stage0
2024-02-18 14:14:55 -08:00
Leonardo de Moura
cd9648a61e
fix: dsimp zeta bug
...
Before the `zeta` / `zetaDelta` split, `dsimp` was performing `zeta`
by going inside of a `let`-expression, performing `zetaDelta`, and
then removing the unused `let`-expression.
2024-02-18 14:14:55 -08:00
Leonardo de Moura
55ce5d570c
chore: add temporary workaround
2024-02-18 14:14:55 -08:00
Leonardo de Moura
ead14987bc
chore: set zetaDelta := true at simp_wf
2024-02-18 14:14:55 -08:00
Leonardo de Moura
834b515592
chore: update stage0
2024-02-18 14:14:55 -08:00
Leonardo de Moura
9fe72c5f95
chore: set zetaDelta := false by default in the simplifier
2024-02-18 14:14:55 -08:00
Leonardo de Moura
77de817960
chore: update stage0
2024-02-18 14:14:55 -08:00
Leonardo de Moura
457d33d660
feat: configuration options zeta and zetaDelta
...
TODO: bootstrapping issues, set `zetaDelta := false` in the simplifier.
2024-02-18 14:14:55 -08:00
Leonardo de Moura
b882ebcf4a
chore: update stage0
2024-02-18 14:14:55 -08:00
Leonardo de Moura
602b1a0d15
feat: add zetaDelta configuration option
2024-02-18 14:14:55 -08:00
Joachim Breitner
17c7cb0e1c
feat: conv => fun ( #3240 )
...
Given a target
```
| f a b
```
the new conv tactic
```
conv => fun
```
turns it into
```
| f a
```
and `arg 0` turns it into
```
| f
```
Fixes #3239
2024-02-18 12:02:25 +00:00
