Zulip Chat Archive
Stream: mathlib4
Topic: PR #15691
Anne Baanen (Nov 23 2022 at 10:55):
I believe the compute_degree tactic in PR #15691 (for mathlib 3) is as good as ready to merge. I don't want to annoy the porting effort so would someone with Lean 4 metaprogramming experience like to check this PR is not too problematic?
Last updated: Dec 20 2023 at 11:08 UTC