Documentation

def Lean.Parser.Syntax.addPrec :

def Lean.Parser.Syntax.subPrec :

def Lean.Parser.Syntax.addPrio :

def Lean.Parser.Syntax.subPrio :

def precMax :

def precArg :

def precLead :

def «prec(_)» :

def precMin :

def precMin1 :

def termMax_prec :

def prioDefault :

def prioLow :

def prioMid :

def prioHigh :

def «prio(_)» :

def «stx_+» :

def «stx_*» :

def stx_? :

def «stx_<|>_» :

def «stx_,*» :

def «stx_,+» :

def «stx_,*,?» :

def «stx_,+,?» :

def stx!_ :

def rawNatLit :

def «term_∘_» :

def «term_×_» :

def «term_|||_» :

def «term_^^^_» :

def «term_&&&_» :

def «term_+_» :

def «term_-_» :

def «term_*_» :

def «term_/_» :

def «term_%_» :

def «term_<<<_» :

def «term_>>>_» :

def «term_^_» :

def «term_++_» :

def «term-_» :

def «term~~~_» :

def «term_<=_» :

def «term_≤_» :

def «term_<_» :

def «term_>=_» :

def «term_≥_» :

def «term_>_» :

def «term_=_» :

def «term_==_» :

def «term_/\_» :

def «term_∧_» :

def «term_\/_» :

def «term_∨_» :

def «term¬_» :

def «term_&&_» :

def «term_||_» :

def term!_ :

def «term_::_» :

def «term_<|>_» :

def «term_>>_» :

def «term_>>=_» :

def «term_<*>_» :

def «term_<*_» :

def «term_*>_» :

def «term_<$>_» :

def termDepIfThenElse :

def termIfThenElse :

def «termIfLet_:=_Then_Else_» :

def «term_<|_» :

def «term_|>_» :

def «term_$__» :

def «term{__:_//_}» :

def termWithout_expected_type_ :

def «term[_]» :

def «term%[_|_]» :

def Lean.term_Matches_ :

def Lean.termThis :

def Lean.Parser.Tactic.intro :

def Lean.Parser.Tactic.intros :

def Lean.Parser.Tactic.rename :

def Lean.Parser.Tactic.revert :

def Lean.Parser.Tactic.clear :

def Lean.Parser.Tactic.subst :

def Lean.Parser.Tactic.assumption :

def Lean.Parser.Tactic.contradiction :

def Lean.Parser.Tactic.apply :

def Lean.Parser.Tactic.exact :

def Lean.Parser.Tactic.refine :

def Lean.Parser.Tactic.refine' :

def Lean.Parser.Tactic.constructor :

def Lean.Parser.Tactic.case :

def Lean.Parser.Tactic.«tacticNext___=>_» :

def Lean.Parser.Tactic.allGoals :

def Lean.Parser.Tactic.anyGoals :

def Lean.Parser.Tactic.focus :

def Lean.Parser.Tactic.skip :

def Lean.Parser.Tactic.done :

def Lean.Parser.Tactic.traceState :

def Lean.Parser.Tactic.failIfSuccess :

def Lean.Parser.Tactic.paren :

def Lean.Parser.Tactic.withReducible :

def Lean.Parser.Tactic.withReducibleAndInstances :

def Lean.Parser.Tactic.first :

def Lean.Parser.Tactic.rotateLeft :

def Lean.Parser.Tactic.rotateRight :

def Lean.Parser.Tactic.tacticTry_ :

def Lean.Parser.Tactic.«tactic_<;>_» :

def Lean.Parser.Tactic.tacticRfl :

def Lean.Parser.Tactic.tacticAdmit :

def Lean.Parser.Tactic.tacticSorry :

def Lean.Parser.Tactic.tacticInfer_instance :

def Lean.Parser.Tactic.config :

def Lean.Parser.Tactic.locationWildcard :

def Lean.Parser.Tactic.locationHyp :

def Lean.Parser.Tactic.location :

def Lean.Parser.Tactic.change :

def Lean.Parser.Tactic.changeWith :

def Lean.Parser.Tactic.rwRule :

def Lean.Parser.Tactic.rwRuleSeq :

def Lean.Parser.Tactic.rewriteSeq :

def Lean.Parser.Tactic.rwSeq :

def Lean.Parser.Tactic.rwWithRfl (kind : Lean.SyntaxNodeKind) (atom : String) (stx : Lean.Syntax) :

def Lean.Parser.Tactic.expandRwSeq :

def Lean.Parser.Tactic.injection :

def Lean.Parser.Tactic.injections :

def Lean.Parser.Tactic.discharger :

def Lean.Parser.Tactic.simpPre :

def Lean.Parser.Tactic.simpPost :

def Lean.Parser.Tactic.simpLemma :

def Lean.Parser.Tactic.simpErase :

def Lean.Parser.Tactic.simpStar :

def Lean.Parser.Tactic.simp :

def Lean.Parser.Tactic.simpAll :

def Lean.Parser.Tactic.delta :

def Lean.Parser.Tactic.unfold :

def Lean.Parser.Tactic.tacticRefine_lift_ :

def Lean.Parser.Tactic.tacticHave_ :

def Lean.Parser.Tactic.«tacticHave__:=_» :

def Lean.Parser.Tactic.tacticSuffices_ :

def Lean.Parser.Tactic.tacticLet_ :

def Lean.Parser.Tactic.tacticShow_ :

def Lean.Parser.Tactic.letrec :

def Lean.Parser.Tactic.tacticRefine_lift'_ :

def Lean.Parser.Tactic.tacticHave'_ :

def Lean.Parser.Tactic.«tacticHave'__:=_» :

def Lean.Parser.Tactic.tacticLet'_ :

def Lean.Parser.Tactic.inductionAlt :

def Lean.Parser.Tactic.inductionAlts :

def Lean.Parser.Tactic.induction :

def Lean.Parser.Tactic.generalizeArg :

def Lean.Parser.Tactic.generalize :

def Lean.Parser.Tactic.casesTarget :

def Lean.Parser.Tactic.cases :

def Lean.Parser.Tactic.existsIntro :

def Lean.Parser.Tactic.renameI :

def Lean.Parser.Tactic.tacticRepeat_ :

def Lean.Parser.Tactic.tacticTrivial :

def Lean.Parser.Tactic.split :

def Lean.Parser.Tactic.specialize :

def Lean.Parser.Tactic.tacticUnhygienic_ :

def Lean.Parser.Attr.simp :

def «term‹_›» :