Zulip Chat Archive

Stream: mathlib4

Topic: Tatic equivalent


Alice Laroche (Feb 03 2022 at 14:14):

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

Arthur Paulino (Feb 03 2022 at 14:38):

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 (Feb 03 2022 at 17:20):

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 (Feb 03 2022 at 17:28):

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:)


Last updated: Dec 20 2023 at 11:08 UTC