Scott Morrison
88deb34ddb
chore: upstream omega ( #3367 )
...
Co-authored-by: Joe Hendrix <joe@lean-fro.org>
2024-02-19 00:19:55 +00:00
Scott Morrison
11727a415b
chore: upstream ext
...
and_intros and subst_eqs are not builtin
clarify failure modes
Clarify docString of extCore
clarify
chore: builtin `subst_eqs` tactic
chore: builtin `ext`
2024-02-15 13:26:01 +01:00
Scott Morrison
329e00661a
chore: upstream Std.Util.ExtendedBinders ( #3320 )
...
This is not a complete upstreaming of that file (it also supports `∀ᵉ (x
< 2) (y < 3), p x y` as shorthand for `∀ x < 2, ∀ y < 3, p x y`, but I
don't think we need this; it is used in Mathlib).
Syntaxes still need to be made built-in.
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
2024-02-14 11:36:00 +00:00
Joe Hendrix
8b0dd2e835
chore: upstream Std.Logic ( #3312 )
...
This will collect definitions from Std.Logic
---------
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
2024-02-14 09:40:55 +00:00
Scott Morrison
90b08ef22e
feat: upstream guard_expr ( #3297 )
...
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
2024-02-11 23:25:04 +00:00
Scott Morrison
4718af5474
chore: upstream rcases ( #3292 )
...
This moves the `rcases` and `obtain` tactics from Std, and makes them
built-in tactics.
We will separately move the test cases from Std after #3297
(`guard_expr`).
---------
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
2024-02-10 05:22:02 +00:00
Leonardo de Moura
09a43990aa
refactor: move if-then-else tactic to Init
2024-02-09 09:57:57 +11:00
Leonardo de Moura
a2aadee28f
feat: simproc declaration vs simproc attribute
...
Allow `simproc`s to be declared without setting the `[simproc]`
attribute. A `simproc` declaration is function + pattern.
Motivation: allow them to be provided as arguments to `simp` **and** `simp only`.
TODO: track their use in `simp`.
TODO: builtin simprocs
2024-01-09 12:57:15 +01:00
Leonardo de Moura
175a6ab606
refactor: add Init/MetaTypes to workaround bootstrapping issues
...
Motivation: we could not set `simp` configuration options at `WFTactics.lean`
2023-10-29 09:38:23 -07:00
Mario Carneiro
158e182b8b
chore: move Bootstrap.Dynamic -> Init.Dynamic
2022-09-02 04:36:54 -07:00
Mario Carneiro
b2b02295b0
chore: move ShareCommon to Init / Lean
2022-08-30 07:51:43 -07:00
Leonardo de Moura
8d9428261e
chore: remove Fix.lean
...
see #1208
2022-06-16 15:30:47 -07:00
Leonardo de Moura
ecbc59c8d8
chore: split Notation.lean
2022-05-09 05:20:19 -07:00
Sebastian Ullrich
ff097e952f
chore: link orphan file
2022-03-07 10:59:49 +01:00
Leonardo de Moura
dae3489fe2
feat: remove partials from Init/Data/Array/Basic.lean
2022-01-10 16:05:33 -08:00
Leonardo de Moura
70f2200778
chore: remove enum command
...
Now, `inductive` is also efficient for big enumeration types
2021-09-06 12:01:37 -07:00
Leonardo de Moura
6f075e6ece
feat: add enum command for declaring enumeration types
...
closes #654
2021-09-05 16:58:49 -07:00
Leonardo de Moura
6d8058034a
chore: basic conv mode parsers
2021-09-01 15:35:32 -07:00
Leonardo de Moura
4ec85a39a5
fix: Not should not be reducible, special support for Ne
...
Unification hint for `Not`
2021-02-15 17:36:11 -08:00
Leonardo de Moura
244b72befd
feat: simpArrow
2021-01-01 17:15:15 -08:00
Leonardo de Moura
df0e4808ec
feat: define tactic parsers using syntax command
2020-11-17 13:52:36 -08:00
Leonardo de Moura
99fad9fc4d
feat: goodies for writing notation with binders
2020-11-14 07:32:44 -08:00
Leonardo de Moura
8c4ac7ccc1
refactor: rename LeanInit ==> Meta, and reduce dependencies
2020-11-13 16:00:31 -08:00
Leonardo de Moura
5c33440050
chore: update Init.lean
2020-11-12 13:23:18 -08:00
Leonardo de Moura
0f3bd8abb4
feat: add rfl and decide! tactic macros
2020-10-29 16:42:22 -07:00
Leonardo de Moura
2dd1d3ac3e
chore: move ShareCommon to Std
2020-06-25 11:45:29 -07:00
Sebastian Ullrich
6a0410f8f0
feat: make import A import A.olean instead of A/Default.olean
2020-05-19 11:29:32 -07:00
