Zulip Chat Archive

Stream: metaprogramming / tactics

Topics:

Positivity extension for Finset.card (58 messages, latest: Dec 14 2023 at 15:22)
Detecting if interactive (7 messages, latest: Dec 11 2023 at 17:34)
Inaccessible optional stuff (25 messages, latest: Dec 06 2023 at 04:10)
Forward chaining with aesop (7 messages, latest: Dec 02 2023 at 11:15)
Polimorphic lam Expr (7 messages, latest: Dec 01 2023 at 21:16)
ring and scalar multiplication (5 messages, latest: Nov 27 2023 at 09:31)
Modifying the reassoc attribute for monadic computations (24 messages, latest: Nov 17 2023 at 05:55)
Hide intermediate goals from user? (3 messages, latest: Nov 16 2023 at 17:30)
Help with writing tactic (213 messages, latest: Nov 06 2023 at 09:16)
Issue writing a tactic (8 messages, latest: Nov 04 2023 at 16:41)
Unexpander trouble (15 messages, latest: Nov 01 2023 at 21:59)
✔ destructured subtype pattern-match syntax (16 messages, latest: Oct 30 2023 at 13:23)
Unexpanders: Book examples fail (4 messages, latest: Oct 28 2023 at 01:27)
Determining whether a definition is recursive (11 messages, latest: Oct 25 2023 at 13:15)
What to specify for addSuggestion (22 messages, latest: Oct 19 2023 at 21:29)
Implicit Arguments in Rewrites (3 messages, latest: Oct 09 2023 at 09:27)
Confusion with Pos.asNat traversing application (1 message, latest: Oct 08 2023 at 21:35)
Taming positivity (45 messages, latest: Sep 17 2023 at 10:09)
✔ get all keys of attributes (3 messages, latest: Jul 30 2023 at 13:40)
ifdef or macro templates (3 messages, latest: Jul 25 2023 at 01:17)
Pattern matching optional Syntax (5 messages, latest: Jul 13 2023 at 16:35)
✔ multiline and indentation based syntax (2 messages, latest: Jul 13 2023 at 02:03)
Metavariables in types of local hypotheses (9 messages, latest: Jul 12 2023 at 14:06)
location of current decl (3 messages, latest: Jun 27 2023 at 11:55)
Meta4dummies (3 messages, latest: Jun 08 2023 at 16:37)
Alternative "toMessageData" for a list (7 messages, latest: Jun 04 2023 at 22:34)
extractGoal (16 messages, latest: Jun 03 2023 at 20:48)
meta tactic mode in Lean4? (11 messages, latest: Jun 03 2023 at 20:40)
Dependent Arrows vs Fun (from MetaProgramming Book) (32 messages, latest: May 23 2023 at 11:39)
Check type of a name (2 messages, latest: May 14 2023 at 19:21)
✔ aliasing a list of tactics (4 messages, latest: Apr 04 2023 at 05:47)
✔ abstract_local (5 messages, latest: Mar 01 2023 at 15:35)
Working with Qq (1 message, latest: Feb 23 2023 at 01:35)
How can I find if a subexpression occurs in a lean theo… (6 messages, latest: Feb 17 2023 at 10:54)
Communicate between successive tactics (7 messages, latest: Jan 27 2023 at 12:15)
Generating globally unique identifiers (4 messages, latest: Dec 12 2022 at 23:19)
lift tries to clear hypotheses (8 messages, latest: Dec 09 2022 at 00:16)
compare API (5 messages, latest: Dec 05 2022 at 01:43)
json strings with newlines (7 messages, latest: Dec 01 2022 at 05:49)
automatic lemmas retrieval (15 messages, latest: Nov 18 2022 at 14:03)
register private name (2 messages, latest: Nov 17 2022 at 21:38)
positivity fails (2 messages, latest: Nov 17 2022 at 21:37)
✔ Pattern matching on ite (3 messages, latest: Oct 14 2022 at 19:12)
namespace, alias and open_locale (4 messages, latest: Oct 14 2022 at 07:31)
Help on metaprogramming (5 messages, latest: Oct 10 2022 at 02:10)
push_neg user command (3 messages, latest: Oct 06 2022 at 17:11)
Call tactic by name (17 messages, latest: Oct 05 2022 at 22:10)
New tactic: positivity (136 messages, latest: Oct 05 2022 at 15:59)
✔ Making a tactic more efficient (11 messages, latest: Sep 28 2022 at 13:51)
Making a tactic more efficient (13 messages, latest: Sep 28 2022 at 13:47)
Variants on mono (5 messages, latest: Sep 25 2022 at 13:48)
Recursing with several tactics (15 messages, latest: Sep 23 2022 at 19:25)
✔ Tactic failure in a class (1 message, latest: Sep 23 2022 at 16:59)
Selectively weaken norm_num (4 messages, latest: Sep 21 2022 at 22:58)
alternative normal form for push_neg (4 messages, latest: Sep 21 2022 at 21:34)
Tactic failure in a class (16 messages, latest: Sep 20 2022 at 18:38)
advice on a tactic for decomposing inequalities (3 messages, latest: Sep 18 2022 at 16:09)
eval_expr and universes (6 messages, latest: Sep 15 2022 at 09:33)
apply_instance fails to infer instance? (17 messages, latest: Sep 12 2022 at 13:33)
is_Type (8 messages, latest: Aug 31 2022 at 08:50)
Match function application (6 messages, latest: Aug 24 2022 at 13:51)
Interval arithmetic – what approach? (21 messages, latest: Aug 24 2022 at 09:18)
norm_num on ennreal (28 messages, latest: Aug 03 2022 at 00:16)
A tactic for expanding matrices into coefficients (17 messages, latest: Jul 28 2022 at 15:44)
letI/exactI within do notation (4 messages, latest: Jul 28 2022 at 13:47)
✔ unexpected (by me) eval_expr behaviour (3 messages, latest: Jul 19 2022 at 02:53)
inversion (6 messages, latest: Jul 14 2022 at 17:15)
✔ Parsing strings with def or theorem keywords (2 messages, latest: Jul 14 2022 at 16:55)
Parsing strings with def or theorem keywords (7 messages, latest: Jul 14 2022 at 15:36)
List of projections of structure (6 messages, latest: Jul 12 2022 at 13:52)
✔ structure with no fields is not a structure (1 message, latest: Jul 12 2022 at 12:52)
structure with no fields is not a structure (8 messages, latest: Jul 10 2022 at 10:03)
current file name (10 messages, latest: Jul 06 2022 at 18:10)
variant syntax for congr' (96 messages, latest: Jun 30 2022 at 16:47)
Instance diamonds in has_to_pexpr (6 messages, latest: Jun 22 2022 at 19:11)
Custom binder (3 messages, latest: Jun 21 2022 at 15:28)
✔ WHNF of partially applied constants (3 messages, latest: Jun 15 2022 at 07:08)
WHNF of partially applied constants (6 messages, latest: Jun 14 2022 at 19:07)
tactic vs option (7 messages, latest: Jun 14 2022 at 09:36)
avoid const_name? (25 messages, latest: Jun 13 2022 at 18:17)
Backtracking parsers (32 messages, latest: Jun 10 2022 at 13:21)
filtering an expr list for matches (12 messages, latest: Jun 10 2022 at 07:33)
if exists assumption else (19 messages, latest: Jun 08 2022 at 11:52)
listing explicit argument types (7 messages, latest: Jun 07 2022 at 15:38)
to_expr behaves differently with an expected type (61 messages, latest: May 16 2022 at 23:58)
tactic.result (4 messages, latest: May 16 2022 at 11:57)
unification assignment (8 messages, latest: May 13 2022 at 15:18)
naming metavariables after the fact (11 messages, latest: May 12 2022 at 10:51)
passing types (23 messages, latest: May 12 2022 at 03:16)
unify (28 messages, latest: May 10 2022 at 18:45)
recursive tactic (12 messages, latest: May 10 2022 at 15:04)
left-over metavariables (14 messages, latest: May 09 2022 at 01:31)
sorting exprs that "are" nats (23 messages, latest: May 07 2022 at 03:40)
passing functions (35 messages, latest: Apr 28 2022 at 07:15)
loc.wildcard (4 messages, latest: Apr 25 2022 at 18:30)
catching errors? (55 messages, latest: Apr 25 2022 at 17:55)
concatenating and the tactic monad (39 messages, latest: Apr 22 2022 at 12:06)
pattern-matching on a pexpr (4 messages, latest: Apr 22 2022 at 11:15)
using ← inside a list of pexpr (45 messages, latest: Apr 20 2022 at 13:22)
✔ note with involved proof term (2 messages, latest: Apr 16 2022 at 13:49)
note with involved proof term (2 messages, latest: Apr 16 2022 at 12:59)
iterate until no change (16 messages, latest: Apr 15 2022 at 12:15)
Building derive_handlers (4 messages, latest: Mar 28 2022 at 13:14)
with_trace_errors (2 messages, latest: Mar 28 2022 at 12:36)
parsing with ad hoc namespace (2 messages, latest: Mar 25 2022 at 16:51)
interactive tactic printer (1 message, latest: Mar 25 2022 at 13:58)
set tactic (55 messages, latest: Mar 23 2022 at 21:39)
✔ parsing specific ident (1 message, latest: Mar 15 2022 at 14:05)
parsing specific ident (26 messages, latest: Mar 14 2022 at 20:53)
✔ parsing and collecting arguments as string (1 message, latest: Mar 14 2022 at 10:36)
parsing and collecting arguments as string (1 message, latest: Mar 10 2022 at 16:45)
faster interval_cases (6 messages, latest: Feb 28 2022 at 17:53)
repeated exists_congr (15 messages, latest: Feb 20 2022 at 19:06)
trivial case of linear_combination (15 messages, latest: Feb 15 2022 at 23:23)
✔ exact name (1 message, latest: Feb 08 2022 at 12:02)
type instance failing with subtype (2 messages, latest: Feb 08 2022 at 10:28)
exact name (7 messages, latest: Feb 07 2022 at 21:31)
parsing type class instance (10 messages, latest: Feb 03 2022 at 10:34)
all axioms used (20 messages, latest: Jan 31 2022 at 15:31)
✔ local_uniq_name providing strange names (3 messages, latest: Jan 30 2022 at 12:33)
convert: why does it use reflexivity transparency.none? (4 messages, latest: Jan 29 2022 at 19:17)
#2890 equiv_rw fails with metavariables (2 messages, latest: Jan 29 2022 at 17:38)
unknown identifier error with user_notation (1 message, latest: Jan 29 2022 at 08:00)
✔ expression printer implemented in pure Lean (1 message, latest: Jan 28 2022 at 10:06)
✔ infer_type decl.value different from decl.type (4 messages, latest: Jan 28 2022 at 10:05)
infer_type decl.value different from decl.type (9 messages, latest: Jan 28 2022 at 07:56)
squeeze_simp - match failed?! (76 messages, latest: Jan 27 2022 at 19:26)
expression printer implemented in pure Lean (9 messages, latest: Jan 26 2022 at 10:34)
assumption with suggestions (31 messages, latest: Jan 25 2022 at 23:33)
filter_upwards (17 messages, latest: Jan 25 2022 at 10:52)
implicit of equality or iff (36 messages, latest: Jan 23 2022 at 16:39)
See what a tactic does and roll back (8 messages, latest: Jan 19 2022 at 19:03)
How does texpr parse numerals? (2 messages, latest: Jan 16 2022 at 07:27)
Expressing parsing (34 messages, latest: Jan 15 2022 at 19:27)
Code review for small tactic (28 messages, latest: Jan 11 2022 at 20:03)
simulating interactive tactics in metaprogramming (18 messages, latest: Jan 11 2022 at 10:35)
tactic parser (4 messages, latest: Jan 11 2022 at 02:31)
interactive save_widget (42 messages, latest: Jan 07 2022 at 19:16)
app builder unification problem (3 messages, latest: Dec 13 2021 at 15:37)
observe (6 messages, latest: Nov 24 2021 at 14:02)
get attributes on decl (5 messages, latest: Nov 11 2021 at 10:40)
Teaching norm_num about complex numbers (20 messages, latest: Nov 09 2021 at 05:14)
decl_noncomputable_reason (4 messages, latest: Oct 30 2021 at 10:48)
Using the vm monad (7 messages, latest: Oct 25 2021 at 12:50)
linarith tactic code (14 messages, latest: Oct 18 2021 at 15:48)
using another tactic inside a meta function (8 messages, latest: Oct 17 2021 at 17:28)
rcases quotient (14 messages, latest: Sep 17 2021 at 03:49)
Testing has_repr (5 messages, latest: Aug 14 2021 at 14:48)
Debugging tactic errors (8 messages, latest: Jul 06 2021 at 14:44)
auto specialize (30 messages, latest: Jul 02 2021 at 11:02)
linarith preprocessing (7 messages, latest: Jul 02 2021 at 06:31)
Tactics outputting to STDOUT (4 messages, latest: Jun 16 2021 at 15:22)
delayed_abstraction meta-variables (10 messages, latest: Jun 15 2021 at 22:29)
Check for sorry in tactic proof (40 messages, latest: Jun 08 2021 at 20:58)
writing large files (11 messages, latest: May 31 2021 at 19:56)
io.iterate/forever and the state_t monad (7 messages, latest: May 31 2021 at 14:54)
parser should fail (11 messages, latest: May 18 2021 at 16:41)
Inaccessible names in tactic state (5 messages, latest: May 18 2021 at 15:26)
nontriviality (17 messages, latest: May 18 2021 at 12:16)
Capturing metavariable assignment (3 messages, latest: May 11 2021 at 13:01)
cases' confuses the equation compiler (2 messages, latest: May 11 2021 at 13:00)
User attribute caching (8 messages, latest: May 07 2021 at 17:21)
how am I getting infinite recursion? (12 messages, latest: Apr 30 2021 at 15:52)
error tolerant string parsing (13 messages, latest: Apr 22 2021 at 08:25)
string replace (9 messages, latest: Apr 22 2021 at 00:51)
help with rewriting simple tactic (1 message, latest: Apr 21 2021 at 19:54)
match expression with unification (7 messages, latest: Apr 19 2021 at 09:42)
finding terms of a certain type in a expr (13 messages, latest: Mar 03 2021 at 18:57)
expr.mfold with branch pruning (19 messages, latest: Mar 02 2021 at 22:39)
Introspecting a definition in a tactic (25 messages, latest: Feb 18 2021 at 09:59)
Allowing focussing on multiple goals in case (15 messages, latest: Jan 27 2021 at 09:54)
printing expr (4 messages, latest: Jan 24 2021 at 22:17)
parse string literal (3 messages, latest: Jan 24 2021 at 14:02)
Flat rintro (51 messages, latest: Jan 22 2021 at 18:41)
parser documentation (5 messages, latest: Jan 22 2021 at 15:14)
to_expr with hint (34 messages, latest: Jan 19 2021 at 19:51)
change all goals (11 messages, latest: Jan 19 2021 at 15:29)
simp with custom congruence lemmas (3 messages, latest: Jan 15 2021 at 10:42)
Fetching all types with instances (37 messages, latest: Jan 14 2021 at 19:33)
Should I use note invisibly (7 messages, latest: Jan 13 2021 at 15:15)
generating a has_coe_to_fun in a tactic (7 messages, latest: Jan 08 2021 at 00:33)
expr structure for coe_fun (16 messages, latest: Jan 08 2021 at 00:33)
(no topic) (1 message, latest: Jan 07 2021 at 01:37)
rw / clear - ident? (10 messages, latest: Jan 06 2021 at 11:21)
tactic.induction does not keep case names (8 messages, latest: Jan 05 2021 at 19:35)
parsing a list of expressions (3 messages, latest: Jan 02 2021 at 18:04)
mk_app fails to retrieve declaration (18 messages, latest: Dec 20 2020 at 22:20)
Allowing multiple targets in case (1 message, latest: Dec 18 2020 at 11:01)
all_some vs traverse id (12 messages, latest: Dec 15 2020 at 15:00)
norm_cast for algebras (8 messages, latest: Nov 25 2020 at 15:28)
Autogenerating differentiable.exp etc (6 messages, latest: Nov 06 2020 at 23:07)
cancel_denoms exercise (54 messages, latest: Nov 06 2020 at 17:57)
access named arguments of declaration (36 messages, latest: Oct 29 2020 at 10:00)
apply name (3 messages, latest: Oct 28 2020 at 13:29)
has_lt for small inductive types (37 messages, latest: Oct 28 2020 at 10:42)
get all lemmas in namespace (6 messages, latest: Oct 28 2020 at 08:44)
elaborate pexpr into expr (18 messages, latest: Oct 27 2020 at 16:34)
instance search in tactic (7 messages, latest: Oct 27 2020 at 14:05)
Linear algebra tactic (26 messages, latest: Oct 20 2020 at 16:25)
congr' is slow (35 messages, latest: Oct 20 2020 at 01:08)
matching binders (20 messages, latest: Oct 18 2020 at 17:31)
mutual recursion (11 messages, latest: Oct 18 2020 at 17:25)
[Automatic apply lemmas for equivalences (and other bundle…](topic/Automatic.20apply.20lemmas.20for.20equivalences.20(and.20other.20bundle.2E.2E.2E.html) (24 messages, latest: Oct 18 2020 at 07:57)
instances for meta defs (80 messages, latest: Oct 13 2020 at 10:18)
Dependencies and local defs (2 messages, latest: Oct 13 2020 at 09:59)
lemma distribution (12 messages, latest: Oct 05 2020 at 08:17)
missing functionality in abel (2 messages, latest: Sep 30 2020 at 04:41)
norm_num for modules (4 messages, latest: Sep 29 2020 at 10:25)
cancel_denoms for vector spaces? (6 messages, latest: Sep 29 2020 at 07:34)
Replacing the result (22 messages, latest: Sep 28 2020 at 17:12)
Trace to stdout (9 messages, latest: Sep 22 2020 at 19:50)
tactic modes(?) (61 messages, latest: Sep 19 2020 at 00:06)
reformulate (17 messages, latest: Sep 16 2020 at 17:06)
No-confusion for generalised inductive types (11 messages, latest: Sep 13 2020 at 14:25)
succ_less tactic (10 messages, latest: Sep 13 2020 at 12:35)
Tactics and universes (22 messages, latest: Sep 11 2020 at 15:35)
Possible cause: occurs check failed (7 messages, latest: Sep 10 2020 at 00:06)
measurable (1 message, latest: Aug 25 2020 at 12:41)
basic parser use (34 messages, latest: Aug 07 2020 at 11:30)
Registering a new option (5 messages, latest: Jul 21 2020 at 01:27)
? exercises (161 messages, latest: Jul 20 2020 at 11:32)
dec_trivial (3 messages, latest: Jul 20 2020 at 08:15)
to_expr failure (4 messages, latest: Jul 18 2020 at 15:32)
constant polynomial tactic (14 messages, latest: Jun 21 2020 at 01:30)
Getting started (7 messages, latest: May 24 2020 at 14:30)
Lean Best Practices (10 messages, latest: May 23 2020 at 07:20)
ideas for exercises (1 message, latest: May 17 2020 at 16:30)
stream events (31 messages, latest: May 17 2020 at 14:19)

Last updated: Dec 20 2023 at 11:08 UTC