Tactics to be ported to mathlib4

Stream: lean4

[Siddharth Bhat]

Does mathport/issues track the progress of porting mathlib tactics toLean4?

[Arthur Paulino]

Tactics are being ported here: https://github.com/leanprover-community/mathlib4
This file contains the syntax for tactics that haven't been implemented yet

[Siddharth Bhat]

Thanks! Where are the tactics that have been implemented, so I can refer to them?

[Arthur Paulino]

Here: https://github.com/leanprover-community/mathlib4/tree/master/Mathlib/Tactic

[Siddharth Bhat]

And I imagine that something like (https://github.com/leanprover-community/mathlib/blob/master/src/tactic/slice.lean) is the corresponding mathlib implementation?