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 required
• B: Hard, because it is a big and complicated tactic
• S: Possibly easy, because we can just stub it out or replace with something else
• ?: uncategorized

ink

def Lean.Parser.Command.include : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.omit : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.parameter : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.propagateTags : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.mapply : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.tacticDestruct_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.abstract : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.cc : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.cc = Lean.ParserDescr.node `Lean.Parser.Tactic.cc 1024 (Lean.ParserDescr.nonReservedSymbol "cc" false)

ink

def Lean.Parser.Tactic.unfoldProjs : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.rsimp : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.rsimp = Lean.ParserDescr.node `Lean.Parser.Tactic.rsimp 1024 (Lean.ParserDescr.nonReservedSymbol "rsimp" false)

ink

def Lean.Parser.Tactic.compVal : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.compVal = Lean.ParserDescr.node `Lean.Parser.Tactic.compVal 1024 (Lean.ParserDescr.nonReservedSymbol "comp_val" false)

ink

def Lean.Parser.Tactic.async : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.injectionsAndClear : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.injectionsAndClear = Lean.ParserDescr.node `Lean.Parser.Tactic.injectionsAndClear 1024 (Lean.ParserDescr.nonReservedSymbol "injections_and_clear" false)

ink

def Lean.Parser.Tactic.tryFor : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.unfoldCoes : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.unfoldWf : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.unfoldWf = Lean.ParserDescr.node `Lean.Parser.Tactic.unfoldWf 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_wf" false)

ink

def Lean.Parser.Tactic.unfoldAux : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.unfoldAux = Lean.ParserDescr.node `Lean.Parser.Tactic.unfoldAux 1024 (Lean.ParserDescr.nonReservedSymbol "unfold_aux" false)

ink

def Lean.Parser.Tactic.continue : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.clean : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.refineStruct : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.matchHyp : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.guardTags : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.guardProofTerm : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.failIfSuccess? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.field : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.haveField : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.haveField = Lean.ParserDescr.node `Lean.Parser.Tactic.haveField 1024 (Lean.ParserDescr.nonReservedSymbol "have_field" false)

ink

def Lean.Parser.Tactic.applyField : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.applyField = Lean.ParserDescr.node `Lean.Parser.Tactic.applyField 1024 (Lean.ParserDescr.nonReservedSymbol "apply_field" false)

ink

def Lean.Parser.Tactic.hGeneralize : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.hGeneralize! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.extractGoal : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.extractGoal! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.revertDeps : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.revertAfter : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.revertTargetDeps : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.revertTargetDeps = Lean.ParserDescr.node `Lean.Parser.Tactic.revertTargetDeps 1024 (Lean.ParserDescr.nonReservedSymbol "revert_target_deps" false)

ink

def Lean.Parser.Tactic.clearValue : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.hint : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.hint = Lean.ParserDescr.node `Lean.Parser.Tactic.hint 1024 (Lean.ParserDescr.nonReservedSymbol "hint" false)

ink

def Lean.Parser.Tactic.congrM : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.acChange : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.rcases? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.rintro? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.decide! : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.decide! = Lean.ParserDescr.node `Lean.Parser.Tactic.decide! 1024 (Lean.ParserDescr.nonReservedSymbol "decide!" false)

ink

def Lean.Parser.Tactic.deltaInstance : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.elide : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.unelide : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.clarify : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.safe : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.finish : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.generalizesArg : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.generalizes : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.withPattern : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.cases'' : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.fixingClause : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.generalizingClause : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.induction'' : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.termList : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.itauto : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.itauto! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.lift : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.obviously : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.obviously = Lean.ParserDescr.node `Lean.Parser.Tactic.obviously 1024 (Lean.ParserDescr.nonReservedSymbol "obviously" false)

ink

def Lean.Parser.Tactic.prettyCases : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.prettyCases = Lean.ParserDescr.node `Lean.Parser.Tactic.prettyCases 1024 (Lean.ParserDescr.nonReservedSymbol "pretty_cases" false)

ink

def Lean.Parser.Tactic.assocRw : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.dsimpResult : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.simpResult : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.suggest : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.truncCases : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.applyNormed : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.noncommRing : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.noncommRing = Lean.ParserDescr.node `Lean.Parser.Tactic.noncommRing 1024 (Lean.ParserDescr.nonReservedSymbol "noncomm_ring" false)

ink

def Lean.Parser.Tactic.polyrith : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.omega : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.acMono : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.reassoc : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.reassoc! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.deriveReassocProof : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.deriveReassocProof = Lean.ParserDescr.node `Lean.Parser.Tactic.deriveReassocProof 1024 (Lean.ParserDescr.nonReservedSymbol "derive_reassoc_proof" false)

ink

def Lean.Parser.Tactic.sliceLHS : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.sliceRHS : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.subtypeInstance : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.subtypeInstance = Lean.ParserDescr.node `Lean.Parser.Tactic.subtypeInstance 1024 (Lean.ParserDescr.nonReservedSymbol "subtype_instance" false)

ink

def Lean.Parser.Tactic.group : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.cancelDenoms : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.transport : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.unfoldCases : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.equivRw : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.equivRwType : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.nthRwLHS : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.nthRwRHS : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.rwSearch : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.rwSearch? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.piInstanceDeriveField : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.piInstanceDeriveField = Lean.ParserDescr.node `Lean.Parser.Tactic.piInstanceDeriveField 1024 (Lean.ParserDescr.nonReservedSymbol "pi_instance_derive_field" false)

ink

def Lean.Parser.Tactic.piInstance : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.piInstance = Lean.ParserDescr.node `Lean.Parser.Tactic.piInstance 1024 (Lean.ParserDescr.nonReservedSymbol "pi_instance" false)

ink

def Lean.Parser.Tactic.tidy : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.tidy? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.wlog : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.elementwise : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.elementwise! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.deriveElementwiseProof : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.deriveElementwiseProof = Lean.ParserDescr.node `Lean.Parser.Tactic.deriveElementwiseProof 1024 (Lean.ParserDescr.nonReservedSymbol "derive_elementwise_proof" false)

ink

def Lean.Parser.Tactic.computeDegreeLE : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.computeDegreeLE = Lean.ParserDescr.node `Lean.Parser.Tactic.computeDegreeLE 1024 (Lean.ParserDescr.nonReservedSymbol "compute_degree_le" false)

ink

def Lean.Parser.Tactic.mkDecorations : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.mkDecorations = Lean.ParserDescr.node `Lean.Parser.Tactic.mkDecorations 1024 (Lean.ParserDescr.nonReservedSymbol "mk_decorations" false)

ink

def Lean.Parser.Tactic.isBounded_default : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.isBounded_default = Lean.ParserDescr.node `Lean.Parser.Tactic.isBounded_default 1024 (Lean.ParserDescr.nonReservedSymbol "isBounded_default" false)

ink

def Lean.Parser.Tactic.opInduction : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.mvBisim : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.unitInterval : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.unitInterval = Lean.ParserDescr.node `Lean.Parser.Tactic.unitInterval 1024 (Lean.ParserDescr.nonReservedSymbol "unit_interval" false)

ink

def Lean.Parser.Tactic.measurability : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.measurability! : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.measurability? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.measurability!? : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.padicIndexSimp : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.borelize : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.uniqueDiffWithinAt_Ici_Iic_univ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.ghostFunTac : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.ghostCalc : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.initRing : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.ghostSimp : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.wittTruncateFunTac : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.wittTruncateFunTac = Lean.ParserDescr.node `Lean.Parser.Tactic.wittTruncateFunTac 1024 (Lean.ParserDescr.nonReservedSymbol "witt_truncate_fun_tac" false)

ink

def Lean.Parser.Tactic.pure_coherence : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.pure_coherence = Lean.ParserDescr.node `Lean.Parser.Tactic.pure_coherence 1024 (Lean.ParserDescr.nonReservedSymbol "pure_coherence" false)

ink

def Lean.Parser.Tactic.coherence : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.coherence = Lean.ParserDescr.node `Lean.Parser.Tactic.coherence 1024 (Lean.ParserDescr.nonReservedSymbol "coherence" false)

ink

def Lean.Parser.Tactic.pgameWFTac : Lean.ParserDescr

Equations

• Lean.Parser.Tactic.pgameWFTac = Lean.ParserDescr.node `Lean.Parser.Tactic.pgameWFTac 1024 (Lean.ParserDescr.nonReservedSymbol "pgame_wf_tac" false)

ink

def Lean.Parser.Tactic.moveOp : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.moveMul : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.moveAdd : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.Conv.applyCongr : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Tactic.Conv.slice : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Attr.intro : Lean.ParserDescr

Equations

• Lean.Parser.Attr.intro = Lean.ParserDescr.node `Lean.Parser.Attr.intro 1024 (Lean.ParserDescr.nonReservedSymbol "intro" false)

ink

def Lean.Parser.Attr.intro! : Lean.ParserDescr

Equations

• Lean.Parser.Attr.intro! = Lean.ParserDescr.node `Lean.Parser.Attr.intro! 1024 (Lean.ParserDescr.nonReservedSymbol "intro!" false)

ink

def Lean.Parser.Attr.interactive : Lean.ParserDescr

Equations

• Lean.Parser.Attr.interactive = Lean.ParserDescr.node `Lean.Parser.Attr.interactive 1024 (Lean.ParserDescr.nonReservedSymbol "interactive" false)

ink

def Lean.Parser.Attr.expandExists : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Attr.protectProj : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Attr.notationClass : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Attr.elementwise : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Attr.pp_nodot : Lean.ParserDescr

Equations

• Lean.Parser.Attr.pp_nodot = Lean.ParserDescr.node `Lean.Parser.Attr.pp_nodot 1024 (Lean.ParserDescr.nonReservedSymbol "pp_nodot" false)

ink

def Lean.Parser.Command.addTacticDoc : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.addHintTactic : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.explode : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.listUnusedDecls : Lean.ParserDescr

Equations

• Lean.Parser.Command.listUnusedDecls = Lean.ParserDescr.node `Lean.Parser.Command.listUnusedDecls 1024 (Lean.ParserDescr.symbol "#list_unused_decls")

ink

def Lean.Parser.Command.defReplacer : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.where : Lean.ParserDescr

Equations

• Lean.Parser.Command.where = Lean.ParserDescr.node `Lean.Parser.Command.where 1024 (Lean.ParserDescr.symbol "#where")

ink

def Lean.Parser.Command.reassocAxiom : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.sample : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.printSorryIn : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.assertExists : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.assertNotExists : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.assertInstance : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

ink

def Lean.Parser.Command.assertNoInstance : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.