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:left
M
: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example:have
N
: 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
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.cc = Lean.ParserDescr.node `Lean.Parser.Tactic.cc 1024 (Lean.ParserDescr.nonReservedSymbol "cc" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.rsimp = Lean.ParserDescr.node `Lean.Parser.Tactic.rsimp 1024 (Lean.ParserDescr.nonReservedSymbol "rsimp" false)
Equations
- Lean.Parser.Tactic.compVal = Lean.ParserDescr.node `Lean.Parser.Tactic.compVal 1024 (Lean.ParserDescr.nonReservedSymbol "comp_val" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.injectionsAndClear = Lean.ParserDescr.node `Lean.Parser.Tactic.injectionsAndClear 1024 (Lean.ParserDescr.nonReservedSymbol "injections_and_clear" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.unfoldWf = Lean.ParserDescr.node `Lean.Parser.Tactic.unfoldWf 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_wf" false)
Equations
- Lean.Parser.Tactic.unfoldAux = Lean.ParserDescr.node `Lean.Parser.Tactic.unfoldAux 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_aux" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.haveField = Lean.ParserDescr.node `Lean.Parser.Tactic.haveField 1024 (Lean.ParserDescr.nonReservedSymbol "have_field" false)
Equations
- Lean.Parser.Tactic.applyField = Lean.ParserDescr.node `Lean.Parser.Tactic.applyField 1024 (Lean.ParserDescr.nonReservedSymbol "apply_field" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.revertTargetDeps = Lean.ParserDescr.node `Lean.Parser.Tactic.revertTargetDeps 1024 (Lean.ParserDescr.nonReservedSymbol "revert_target_deps" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.hint = Lean.ParserDescr.node `Lean.Parser.Tactic.hint 1024 (Lean.ParserDescr.nonReservedSymbol "hint" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.decide! = Lean.ParserDescr.node `Lean.Parser.Tactic.decide! 1024 (Lean.ParserDescr.nonReservedSymbol "decide!" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.obviously = Lean.ParserDescr.node `Lean.Parser.Tactic.obviously 1024 (Lean.ParserDescr.nonReservedSymbol "obviously" false)
Equations
- Lean.Parser.Tactic.prettyCases = Lean.ParserDescr.node `Lean.Parser.Tactic.prettyCases 1024 (Lean.ParserDescr.nonReservedSymbol "pretty_cases" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.noncommRing = Lean.ParserDescr.node `Lean.Parser.Tactic.noncommRing 1024 (Lean.ParserDescr.nonReservedSymbol "noncomm_ring" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.deriveReassocProof = Lean.ParserDescr.node `Lean.Parser.Tactic.deriveReassocProof 1024 (Lean.ParserDescr.nonReservedSymbol "derive_reassoc_proof" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.subtypeInstance = Lean.ParserDescr.node `Lean.Parser.Tactic.subtypeInstance 1024 (Lean.ParserDescr.nonReservedSymbol "subtype_instance" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.piInstanceDeriveField = Lean.ParserDescr.node `Lean.Parser.Tactic.piInstanceDeriveField 1024 (Lean.ParserDescr.nonReservedSymbol "pi_instance_derive_field" false)
Equations
- Lean.Parser.Tactic.piInstance = Lean.ParserDescr.node `Lean.Parser.Tactic.piInstance 1024 (Lean.ParserDescr.nonReservedSymbol "pi_instance" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.deriveElementwiseProof = Lean.ParserDescr.node `Lean.Parser.Tactic.deriveElementwiseProof 1024 (Lean.ParserDescr.nonReservedSymbol "derive_elementwise_proof" false)
Equations
- Lean.Parser.Tactic.computeDegreeLE = Lean.ParserDescr.node `Lean.Parser.Tactic.computeDegreeLE 1024 (Lean.ParserDescr.nonReservedSymbol "compute_degree_le" false)
Equations
- Lean.Parser.Tactic.mkDecorations = Lean.ParserDescr.node `Lean.Parser.Tactic.mkDecorations 1024 (Lean.ParserDescr.nonReservedSymbol "mk_decorations" false)
Equations
- Lean.Parser.Tactic.isBounded_default = Lean.ParserDescr.node `Lean.Parser.Tactic.isBounded_default 1024 (Lean.ParserDescr.nonReservedSymbol "isBounded_default" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.unitInterval = Lean.ParserDescr.node `Lean.Parser.Tactic.unitInterval 1024 (Lean.ParserDescr.nonReservedSymbol "unit_interval" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Tactic.wittTruncateFunTac = Lean.ParserDescr.node `Lean.Parser.Tactic.wittTruncateFunTac 1024 (Lean.ParserDescr.nonReservedSymbol "witt_truncate_fun_tac" false)
Equations
- Lean.Parser.Tactic.pure_coherence = Lean.ParserDescr.node `Lean.Parser.Tactic.pure_coherence 1024 (Lean.ParserDescr.nonReservedSymbol "pure_coherence" false)
Equations
- Lean.Parser.Tactic.coherence = Lean.ParserDescr.node `Lean.Parser.Tactic.coherence 1024 (Lean.ParserDescr.nonReservedSymbol "coherence" false)
Equations
- Lean.Parser.Tactic.pgameWFTac = Lean.ParserDescr.node `Lean.Parser.Tactic.pgameWFTac 1024 (Lean.ParserDescr.nonReservedSymbol "pgame_wf_tac" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Attr.intro = Lean.ParserDescr.node `Lean.Parser.Attr.intro 1024 (Lean.ParserDescr.nonReservedSymbol "intro" false)
Equations
- Lean.Parser.Attr.intro! = Lean.ParserDescr.node `Lean.Parser.Attr.intro! 1024 (Lean.ParserDescr.nonReservedSymbol "intro!" false)
Equations
- Lean.Parser.Attr.interactive = Lean.ParserDescr.node `Lean.Parser.Attr.interactive 1024 (Lean.ParserDescr.nonReservedSymbol "interactive" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Attr.pp_nodot = Lean.ParserDescr.node `Lean.Parser.Attr.pp_nodot 1024 (Lean.ParserDescr.nonReservedSymbol "pp_nodot" false)
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Command.listUnusedDecls = Lean.ParserDescr.node `Lean.Parser.Command.listUnusedDecls 1024 (Lean.ParserDescr.symbol "#list_unused_decls")
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Parser.Command.where = Lean.ParserDescr.node `Lean.Parser.Command.where 1024 (Lean.ParserDescr.symbol "#where")
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.