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
Scott Morrison
e206e53f4e
chore: add @[simp] to Nat.sub_add_cancel ( #3378 )
2024-02-18 06:48:10 +00:00
Kyle Miller
d569ed4e5f
feat: make loose fvars pretty print as _fvar.123 instead of _uniq.123 ( #3380 )
...
Loose fvars are never supposed to be pretty printed, but having them
print with "fvar" in the name can help with debugging broken tactics and
elaborators.
Metaprogramming users often do not realize at first that `_uniq.???` in
pretty printing output refers to fvars not in the current local context.
2024-02-18 01:53:37 +00:00
Kyle Miller
433c4d22c2
fix: exposeRelevantUniverses was inserting the whole expression into itself
...
This bug appeared in c9db8619f1
2024-02-17 17:53:19 -08:00
Leonardo de Moura
6383af0595
chore: update stage0
2024-02-17 17:51:24 -08:00
Leonardo de Moura
c8236ccd47
chore: basic simprocs for String
2024-02-17 17:51:24 -08:00
Leonardo de Moura
559a18874c
chore: simprocs for Eq
2024-02-17 17:51:24 -08:00
Leonardo de Moura
3dcc8cab3e
feat: simprocs for Char.val, default char, and Char.ofNatAux
2024-02-17 17:51:24 -08:00
Leonardo de Moura
fb18ef3688
feat: simprocs for UInt??.ofNatCore and UInt??.toNat
2024-02-17 17:51:24 -08:00
Leonardo de Moura
3e5695e07e
feat: simprocs for Char ( #3382 )
2024-02-17 20:36:51 +00:00
Leonardo de Moura
61a76a814f
feat: delaborator for Char literals ( #3381 )
2024-02-17 12:19:40 -08:00
Arthur Adjedj
0c92d17792
fix: instantiate the types of inductives with the right parameters ( #3246 )
...
Closes #3242
2024-02-17 16:52:28 +00:00
Joachim Breitner
d536534c4d
refactor: drop CasesOnApp, use MatcherApp ( #3369 )
...
in all uses of `CasesOnApp`, we treat `MatcherApp`s the same way,
dupliating a fair amount of relatively hairy code (and there is more to
come).
However, the `MatcherApp` abstraction is perfectly capable of
also representing `casesOn` applications, at least for the use cases
encountered so far.
So lets just (optionally) include `casesOn` applications when looking
for matchers,
and remove the `CasesOnApp` abstraction completely.
2024-02-17 15:25:32 +00:00
Leonardo de Moura
97e7e668d6
chore: pp.proofs.withType is now false by default ( #3379 )
...
`pp.proofs.withType := true` often produces too much noise in the info
view.
2024-02-17 15:09:24 +00:00
Sebastian Ullrich
dda88c9926
feat: infoview.maxTraceChildren ( #3370 )
...
Incrementally unveil trace children for excessively large nodes to
improve infoview rendering time, adjust particularly chatty
`simp.ground` trace to make use of it.
2024-02-17 14:04:46 +00:00
Leonardo de Moura
ef9a6bb839
fix: an equation lemma with autoParam arguments fails to rewrite ( #3316 )
...
closes #2243
2024-02-17 13:42:34 +00:00
