Docs about `meta` keyword

Stream: new members

[Anton Kalsin]

I've seen keyword meta, but tutorial doesn't contain info about it. Where can I find documentation about it?

[Johan Commelin]

Have you checked #tpil?

[Patrick Massot]

I don't think this is explained there

[Patrick Massot]

The tactic writing tutorial is a more promising place

[Patrick Massot]

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md

[Mario Carneiro]

I don't think that actually says anything about meta, although it uses it all over the place

[Patrick Massot]

There is a sentence about it

[Patrick Massot]

But it may be cryptic

[Anton Kalsin]

Patrick Massot said:

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/tactic_writing.md

Thanks! This is actually what I was looking for.