Zulip Chat Archive
Stream: triage
Topic: issue #2882: apply_congr with h
Random Issue Bot (Nov 18 2020 at 14:19):
Today I chose issue 2882 for discussion!
apply_congr with h
Created by @Scott Morrison (@semorrison) on 2020-05-31
Labels: enhancement, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Rob Lewis (Nov 18 2020 at 14:23):
This sounds like an easy metaprogramming exercise for anyone who wants a bit of practice!
Random Issue Bot (Feb 03 2022 at 14:17):
Today I chose issue 2882 for discussion!
apply_congr with h
Created by @Scott Morrison (@semorrison) on 2020-05-31
Labels: enhancement, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Arthur Paulino (Feb 03 2022 at 14:27):
I would pick up this one, but I'm focusing on Mathlib4 tactics right now
Johan Commelin (Feb 03 2022 at 14:30):
@Arthur Paulino I think it's easier to port this issue to the mathlib4 repo.
Please continue focussing on mathlib4 tactics. It's really great that you are doing this!
Kevin Buzzard (Feb 04 2022 at 23:01):
@Arthur Paulino did you see https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Recordings.20of.20Lean.20coding.20sessions/near/270689158 ?
Arthur Paulino (Feb 04 2022 at 23:06):
@Kevin Buzzard I hadn't seen it yet. Is that an ordered wishlist for Mathlib4?
Kevin Buzzard (Feb 05 2022 at 00:11):
To be precise, I'm teaching an undergraduate course and it's an ordered wishlist of what I need to port my course to Lean 4. If I had these I could make a mini "introduction to mathematics in Lean 4" course.
Arthur Paulino (Feb 05 2022 at 01:35):
Those are a bit too involved for me at the moment :sweat_smile:
I'll get there eventually
Last updated: Dec 20 2023 at 11:08 UTC