Zulip Chat Archive
Stream: metaprogramming / tactics
Topics:
- 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: Apr 16 2021 at 20:15 UTC