Lean stage0 autoupdater
007b423006
chore: update stage0
2024-05-30 09:57:02 +00:00
Sebastian Ullrich
ba629545cc
chore: update stage0
2024-05-23 17:26:21 +02:00
Leonardo de Moura
6155513c60
chore: update stage0
...
Motivation: `[grind_cases]` at `Init`
2024-05-21 21:46:23 +02:00
Leonardo de Moura
239ade80dc
chore: update stage0
2024-05-19 07:20:10 +02:00
Leonardo de Moura
c8b72beb4d
chore: update stage0
2024-05-19 07:20:10 +02:00
Leonardo de Moura
770235855f
chore: update stage0
2024-05-14 19:52:25 +02:00
Lean stage0 autoupdater
dcdc3db3d4
chore: update stage0
2024-05-10 07:39:47 +00:00
Leonardo de Moura
dfde4ee3aa
chore: update stage0
2024-05-07 03:23:30 +02:00
Leonardo de Moura
7294646eb9
chore: update stage0
2024-04-29 05:46:11 +02:00
Lean stage0 autoupdater
9dcf07203e
chore: update stage0
2024-04-19 08:22:54 +00:00
Lean stage0 autoupdater
11a9d2ee4b
chore: update stage0
2024-04-17 19:26:22 +00:00
Lean stage0 autoupdater
88ee503f02
chore: update stage0
2024-04-17 09:21:10 +00:00
Lean stage0 autoupdater
b0a305f19f
chore: update stage0
2024-04-13 09:49:19 +00:00
Leonardo de Moura
9bdb37a9b0
chore: update stage0
...
Reason: new builtin environment extension
2024-03-28 17:58:33 -07:00
Lean stage0 autoupdater
63290babde
chore: update stage0
2024-03-27 07:34:13 +00:00
Lean stage0 autoupdater
d884a946c8
chore: update stage0
2024-03-22 01:16:40 +00:00
Lean stage0 autoupdater
d5701fc912
chore: update stage0
2024-03-22 00:00:55 +00:00
Lean stage0 autoupdater
4391bc2977
chore: update stage0
2024-03-20 22:45:34 +00:00
Lean stage0 autoupdater
01432ffc5a
chore: update stage0
2024-03-18 12:20:03 +00:00
Lean stage0 autoupdater
f70895ede5
chore: update stage0
2024-03-15 16:30:21 +00:00
Leonardo de Moura
214179b6b9
chore: update stage0
2024-03-13 21:15:48 -07:00
Leonardo de Moura
653eb5f66e
chore: update stage0
2024-03-13 21:15:48 -07:00
Leonardo de Moura
0f19332618
chore: update stage0
2024-03-13 12:37:58 -07:00
Lean stage0 autoupdater
1388f6bc83
chore: update stage0
2024-03-11 17:22:37 +00:00
Kyle Miller
45fccc5906
feat: custom eliminators for induction and cases tactics, and beautiful eliminators for Nat ( #3629 )
...
Replaces `@[eliminator]` with two attributes `@[induction_eliminator]`
and `@[cases_eliminator]` for defining custom eliminators for the
`induction` and `cases` tactics, respectively.
Adds `Nat.recAux` and `Nat.casesAuxOn`, which are eliminators that are
defeq to `Nat.rec` and `Nat.casesOn`, but these use `0` and `n + 1`
rather than `Nat.zero` and `Nat.succ n`.
For example, using `induction` to prove that the factorial function is
positive now has the following goal states (thanks also to #3616 for the
goal state after unfolding).
```lean
example : 0 < fact x := by
induction x with
| zero => decide
| succ x ih =>
/-
x : Nat
ih : 0 < fact x
⊢ 0 < fact (x + 1)
-/
unfold fact
/-
...
⊢ 0 < (x + 1) * fact x
-/
simpa using ih
```
Thanks to @adamtopaz for initial work on splitting the `@[eliminator]`
attribute.
2024-03-09 15:31:51 +00:00
Leonardo de Moura
4208c44939
chore: update stage0
2024-03-06 15:29:04 -08:00
Leonardo de Moura
1da65558d0
chore: update stage0
2024-03-05 14:42:05 -08:00
Leonardo de Moura
ea9a417371
chore: update stage0
2024-03-01 22:33:14 -08:00
Scott Morrison
b762567174
chore: update stage0
2024-02-29 17:34:15 +11:00
Lean stage0 autoupdater
17b8880983
chore: update stage0
2024-02-28 11:50:07 +00:00
Kyle Miller
37fd128f9f
chore: update stage0
2024-02-28 09:23:17 +01:00
Lean stage0 autoupdater
7d5b6cf097
chore: update stage0
2024-02-27 10:00:46 +00:00
Leonardo de Moura
bfb981d465
chore: update stage0
2024-02-25 11:44:42 -08:00
Leonardo de Moura
02e4fe0b1c
chore: update stage0
2024-02-25 11:44:42 -08:00
Scott Morrison
46df6142a6
chore: update stage0
2024-02-22 06:23:26 -08:00
Joe Hendrix
6e821de11a
chore: update stage0
2024-02-21 21:58:54 +01:00
Lean stage0 autoupdater
71cfbb26de
chore: update stage0
2024-02-21 15:19:07 +00:00
Leonardo de Moura
855a762bcb
chore: update stage0
2024-02-20 07:00:47 -08:00
Sebastian Ullrich
79a9f6759a
chore: update stage0
2024-02-20 12:48:19 +01: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
f64d14ea54
chore: update stage0
2024-02-19 12:47:04 -08:00
Lean stage0 autoupdater
7545b85512
chore: update stage0
2024-02-19 15:51:18 +00:00
Sebastian Ullrich
59bf220934
chore: update stage0
2024-02-19 12:37:19 +01:00
Leonardo de Moura
58ed6b9630
chore: update stage0
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
b882ebcf4a
chore: update stage0
2024-02-18 14:14:55 -08:00
Leonardo de Moura
6383af0595
chore: update stage0
2024-02-17 17:51:24 -08:00
Lean stage0 autoupdater
271ae5b8e5
chore: update stage0
2024-02-15 12:32:00 +00:00
Scott Morrison
5a95f91fae
chore: update stage0
2024-02-15 13:26:01 +01:00
Scott Morrison
144c1bbbaf
chore: update stage0
2024-02-15 14:33:36 +11:00
