Zulip Chat Archive

Stream: metaprogramming / tactics

Topics:

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)
Interval arithmetic – what approach? (20 messages, latest: Oct 03 2020 at 08:30)
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)
assumption with suggestions (14 messages, latest: Sep 09 2020 at 21:55)
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)
linarith preprocessing (4 messages, latest: Jul 16 2020 at 14:04)
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: Jun 20 2021 at 04:13 UTC