issue !4#430: tactic porting tracking issue

Stream: triage

[Random Issue Bot]

Today I chose issue 430 for discussion!

tactic porting tracking issue
Created by @Scott Morrison (@semorrison) on 2022-09-20
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Random Issue Bot]

Today I chose issue 430 for discussion!

tactic porting tracking issue
Created by @Kim Morrison (@semorrison) on 2022-09-20
Labels:

Is this issue still relevant? Any recent updates? Anyone making progress?

[Yaël Dillies]

Is there much point to this issue nowadays?

[Kevin Buzzard]

It's a very discoverable place to look for answers to "did this obscure tactic ever get ported?"

[Yaël Dillies]

Sure, but does it need to stay opened?

[Mario Carneiro]

well the tactics on the list are still not ported

[Mario Carneiro]

this doesn't mean they aren't useful, it just means they weren't on the critical path to porting mathlib

[Kevin Buzzard]

Indeed I was just looking at some quite messy mathlib4 code which had a porting note saying that it was all easier in Lean 3 because assoc_rw was a thing there.