Zulip Chat Archive

Stream: new members

Topic: Docs about `meta` keyword


view this post on Zulip Anton Kalsin (May 09 2020 at 14:36):

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

view this post on Zulip Johan Commelin (May 09 2020 at 14:37):

Have you checked #tpil?

view this post on Zulip Patrick Massot (May 09 2020 at 14:38):

I don't think this is explained there

view this post on Zulip Patrick Massot (May 09 2020 at 14:39):

The tactic writing tutorial is a more promising place

view this post on Zulip Patrick Massot (May 09 2020 at 14:39):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 14:40):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:40):

There is a sentence about it

view this post on Zulip Patrick Massot (May 09 2020 at 14:40):

But it may be cryptic

view this post on Zulip Anton Kalsin (May 09 2020 at 14:46):

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.


Last updated: May 08 2021 at 10:12 UTC