This file defines all the tactics that are required by mathport. Most of the syntax declarations
in this file (as opposed to the imported files) are not defined anywhere and effectively form the
TODO list before we can port mathlib to lean 4 for real.
For tactic writers: I (Mario) have put a comment before each syntax declaration to represent the estimated difficulty of writing the tactic. The key is as follows:
E: Easy. It's a simple macro in terms of existing things, or an elab tactic for which we have many similar examples. Example:leftM: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example:haveN: Possibly requires new mechanisms in lean 4, some investigation requiredB: Hard, because it is a big and complicated tacticS: Possibly easy, because we can just stub it out or replace with something else?: uncategorized