Zulip Chat Archive

Stream: lean4

Topic: Writing tactics

Shreyas Srinivas (Feb 14 2023 at 14:45):

How much of this tutorial for writing tactics in lean3 applies to lean4?

Shreyas Srinivas (Feb 14 2023 at 14:46):

Based on the tactics code I have seen in lean4 there are some differences.

Shreyas Srinivas (Feb 14 2023 at 14:47):

the keyword meta seems to have disappeared

Jannis Limperg (Feb 14 2023 at 14:52):

Some of the general concepts may translate, but the details are very different. The metaprogramming book is currently the best tactic writing documentation we have.

Last updated: Dec 20 2023 at 11:08 UTC