Tatic equivalent

Stream: mathlib4

[Alice Laroche]

Is there some equivalent of "pushNeg" in the library ?

[Arthur Paulino]

Not yet. At the moment, there's just a definition of its syntax in Mathlib4: syntax (name := pushNeg) "push_neg" (ppSpace location)? : tactic But it's still unimplemented

Nvm, you asked about an equivalent

[Alice Laroche]

Is there some documentation about lean4 tactic writing somewhere?
I don't plan to implementing it totally , but if I can do some useful tool for me it will be great

[Arthur Paulino]

Not yet. I asked a similar question here. I'm in the process of learning it so I can kick off a bare bones documentation for it, if nobody else does it first

(help is welcome btw :smiley:)