Lean.Parser.Command

source

def Lean.Parser.Term.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Term.quot)) (Lean.Parser.leadingNode `Lean.Parser.Term.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth (HOrElse.hOrElse Lean.Parser.termParser fun x => Lean.Parser.many1Unbox Lean.Parser.commandParser)) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.precheckedQuot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.precheckedQuot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "precheckedQuot" (some `Lean.Parser.Term.precheckedQuot)) (Lean.Parser.leadingNode `Lean.Parser.Term.precheckedQuot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`") fun x => Lean.Parser.Term.quot))

source

def Lean.Parser.Command.terminationHintMany (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationHintMany p = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "terminationHintMany" (some `Lean.Parser.Command.terminationHintMany)) (Lean.Parser.leadingNode `Lean.Parser.Command.terminationHintMany 1024 (HAndThen.hAndThen (Lean.Parser.atomic (Lean.Parser.lookahead (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.symbol " => "))) fun x => Lean.Parser.many1Indent (Lean.Parser.group (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol " => ") fun x => HAndThen.hAndThen p fun x => Lean.Parser.optional (Lean.Parser.symbol ";")))))

source

def Lean.Parser.Command.terminationHint1 (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationHint1 p = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "terminationHint1" (some `Lean.Parser.Command.terminationHint1)) (Lean.Parser.leadingNode `Lean.Parser.Command.terminationHint1 1024 p)

source

def Lean.Parser.Command.terminationHint (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationHint p = HOrElse.hOrElse (Lean.Parser.Command.terminationHintMany p) fun x => Lean.Parser.Command.terminationHint1 p

source

def Lean.Parser.Command.terminationByCore :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationByCore = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "terminationByCore" (some `Lean.Parser.Command.terminationByCore)) (Lean.Parser.leadingNode `Lean.Parser.Command.terminationByCore 1024 (HAndThen.hAndThen (Lean.Parser.symbol "termination_by' ") fun x => Lean.Parser.Command.terminationHint Lean.Parser.termParser))

source

def Lean.Parser.Command.decreasingBy :

Lean.Parser.Parser

Equations

Lean.Parser.Command.decreasingBy = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "decreasingBy" (some `Lean.Parser.Command.decreasingBy)) (Lean.Parser.leadingNode `Lean.Parser.Command.decreasingBy 1024 (HAndThen.hAndThen (Lean.Parser.symbol "decreasing_by ") fun x => Lean.Parser.Command.terminationHint Lean.Parser.Tactic.tacticSeq))

source

def Lean.Parser.Command.terminationByElement :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationByElement = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "terminationByElement" (some `Lean.Parser.Command.terminationByElement)) (Lean.Parser.leadingNode `Lean.Parser.Command.terminationByElement 1024 (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.ident fun x => Lean.Parser.symbol "_") fun x => HAndThen.hAndThen (Lean.Parser.many (HOrElse.hOrElse Lean.Parser.ident fun x => Lean.Parser.symbol "_")) fun x => HAndThen.hAndThen (Lean.Parser.symbol " => ") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.optional (Lean.Parser.symbol ";")))

source

def Lean.Parser.Command.terminationBy :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationBy = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "terminationBy" (some `Lean.Parser.Command.terminationBy)) (Lean.Parser.leadingNode `Lean.Parser.Command.terminationBy 1024 (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen (Lean.Parser.symbol "termination_by ") fun x => Lean.Parser.many1Indent Lean.Parser.Command.terminationByElement))

source

def Lean.Parser.Command.moduleDoc :

Lean.Parser.Parser

Equations

Lean.Parser.Command.moduleDoc = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "moduleDoc" (some `Lean.Parser.Command.moduleDoc)) (Lean.Parser.leadingNode `Lean.Parser.Command.moduleDoc 1024 (Lean.Parser.ppDedent (HAndThen.hAndThen (Lean.Parser.symbol "/-!") fun x => HAndThen.hAndThen Lean.Parser.Command.commentBody fun x => Lean.Parser.ppLine)))

source

def Lean.Parser.Command.terminationSuffix :

Lean.Parser.Parser

Equations

Lean.Parser.Command.terminationSuffix = HAndThen.hAndThen (Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Command.terminationBy fun x => Lean.Parser.Command.terminationByCore)) fun x => Lean.Parser.optional Lean.Parser.Command.decreasingBy

source

def Lean.Parser.Command.namedPrio :

Lean.Parser.Parser

Equations

Lean.Parser.Command.namedPrio = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "namedPrio" (some `Lean.Parser.Command.namedPrio)) (Lean.Parser.leadingNode `Lean.Parser.Command.namedPrio 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => Lean.Parser.nonReservedSymbol "priority")) fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => HAndThen.hAndThen Lean.Parser.priorityParser fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Command.optNamedPrio :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optNamedPrio = Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Command.namedPrio)

source

def Lean.Parser.Command.private :

Lean.Parser.Parser

Equations

Lean.Parser.Command.private = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "private" (some `Lean.Parser.Command.private)) (Lean.Parser.leadingNode `Lean.Parser.Command.private 1024 (Lean.Parser.symbol "private "))

source

def Lean.Parser.Command.protected :

Lean.Parser.Parser

Equations

Lean.Parser.Command.protected = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "protected" (some `Lean.Parser.Command.protected)) (Lean.Parser.leadingNode `Lean.Parser.Command.protected 1024 (Lean.Parser.symbol "protected "))

source

def Lean.Parser.Command.visibility :

Lean.Parser.Parser

Equations

Lean.Parser.Command.visibility = HOrElse.hOrElse Lean.Parser.Command.private fun x => Lean.Parser.Command.protected

source

def Lean.Parser.Command.noncomputable :

Lean.Parser.Parser

Equations

Lean.Parser.Command.noncomputable = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "noncomputable" (some `Lean.Parser.Command.noncomputable)) (Lean.Parser.leadingNode `Lean.Parser.Command.noncomputable 1024 (Lean.Parser.symbol "noncomputable "))

source

def Lean.Parser.Command.unsafe :

Lean.Parser.Parser

Equations

Lean.Parser.Command.unsafe = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "unsafe" (some `Lean.Parser.Command.unsafe)) (Lean.Parser.leadingNode `Lean.Parser.Command.unsafe 1024 (Lean.Parser.symbol "unsafe "))

source

def Lean.Parser.Command.partial :

Lean.Parser.Parser

Equations

Lean.Parser.Command.partial = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "partial" (some `Lean.Parser.Command.partial)) (Lean.Parser.leadingNode `Lean.Parser.Command.partial 1024 (Lean.Parser.symbol "partial "))

source

def Lean.Parser.Command.nonrec :

Lean.Parser.Parser

Equations

Lean.Parser.Command.nonrec = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "nonrec" (some `Lean.Parser.Command.nonrec)) (Lean.Parser.leadingNode `Lean.Parser.Command.nonrec 1024 (Lean.Parser.symbol "nonrec "))

source

def Lean.Parser.Command.declModifiers (inline : Bool) :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declModifiers inline = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "declModifiers" (some `Lean.Parser.Command.declModifiers)) (Lean.Parser.leadingNode `Lean.Parser.Command.declModifiers 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.Term.attributes fun x => if inline = true then Lean.Parser.skip else Lean.Parser.ppDedent Lean.Parser.ppLine)) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.visibility) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.noncomputable) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.unsafe) fun x => Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Command.partial fun x => Lean.Parser.Command.nonrec)))

source

def Lean.Parser.Command.declId :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declId = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "declId" (some `Lean.Parser.Command.declId)) (Lean.Parser.leadingNode `Lean.Parser.Command.declId 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol ".{") fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.ident ", " (Lean.Parser.symbol ", ")) fun x => Lean.Parser.symbol "}")))

source

def Lean.Parser.Command.declSig :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declSig = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "declSig" (some `Lean.Parser.Command.declSig)) (Lean.Parser.leadingNode `Lean.Parser.Command.declSig 1024 (HAndThen.hAndThen (Lean.Parser.many (HAndThen.hAndThen Lean.Parser.ppSpace fun x => HOrElse.hOrElse Lean.Parser.Term.simpleBinderWithoutType fun x => Lean.Parser.Term.bracketedBinder)) fun x => Lean.Parser.Term.typeSpec))

source

def Lean.Parser.Command.optDeclSig :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optDeclSig = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "optDeclSig" (some `Lean.Parser.Command.optDeclSig)) (Lean.Parser.leadingNode `Lean.Parser.Command.optDeclSig 1024 (HAndThen.hAndThen (Lean.Parser.many (HAndThen.hAndThen Lean.Parser.ppSpace fun x => HOrElse.hOrElse Lean.Parser.Term.simpleBinderWithoutType fun x => Lean.Parser.Term.bracketedBinder)) fun x => Lean.Parser.Term.optType))

source

def Lean.Parser.Command.declValSimple :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declValSimple = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "declValSimple" (some `Lean.Parser.Command.declValSimple)) (Lean.Parser.leadingNode `Lean.Parser.Command.declValSimple 1024 (HAndThen.hAndThen (Lean.Parser.symbol " :=") fun x => HAndThen.hAndThen Lean.Parser.ppHardLineUnlessUngrouped fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.optional Lean.Parser.Term.whereDecls))

source

def Lean.Parser.Command.declValEqns :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declValEqns = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "declValEqns" (some `Lean.Parser.Command.declValEqns)) (Lean.Parser.leadingNode `Lean.Parser.Command.declValEqns 1024 Lean.Parser.Term.matchAltsWhereDecls)

source

def Lean.Parser.Command.whereStructField :

Lean.Parser.Parser

Equations

Lean.Parser.Command.whereStructField = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "whereStructField" (some `Lean.Parser.Command.whereStructField)) (Lean.Parser.leadingNode `Lean.Parser.Command.whereStructField 1024 Lean.Parser.Term.letDecl)

source

def Lean.Parser.Command.whereStructInst :

Lean.Parser.Parser

Equations

Lean.Parser.Command.whereStructInst = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "whereStructInst" (some `Lean.Parser.Command.whereStructInst)) (Lean.Parser.leadingNode `Lean.Parser.Command.whereStructInst 1024 (HAndThen.hAndThen (Lean.Parser.symbol " where") fun x => Lean.Parser.many1Indent (HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.ppGroup (Lean.Parser.group (HAndThen.hAndThen Lean.Parser.Command.whereStructField fun x => Lean.Parser.optional (Lean.Parser.symbol ";"))))))

source

def Lean.Parser.Command.declVal :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declVal = HOrElse.hOrElse Lean.Parser.Command.declValSimple fun x => HOrElse.hOrElse Lean.Parser.Command.declValEqns fun x => Lean.Parser.Command.whereStructInst

source

def Lean.Parser.Command.abbrev :

Lean.Parser.Parser

Equations

Lean.Parser.Command.abbrev = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "abbrev" (some `Lean.Parser.Command.abbrev)) (Lean.Parser.leadingNode `Lean.Parser.Command.abbrev 1024 (HAndThen.hAndThen (Lean.Parser.symbol "abbrev ") fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.optDeclSig) fun x => Lean.Parser.Command.declVal))

source

def Lean.Parser.Command.optDefDeriving :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optDefDeriving = Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "deriving ") fun x => Lean.Parser.notSymbol "instance")) fun x => Lean.Parser.sepBy1 Lean.Parser.ident ", " (Lean.Parser.symbol ", "))

source

def Lean.Parser.Command.def :

Lean.Parser.Parser

Equations

Lean.Parser.Command.def = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "def" (some `Lean.Parser.Command.def)) (Lean.Parser.leadingNode `Lean.Parser.Command.def 1024 (HAndThen.hAndThen (Lean.Parser.symbol "def ") fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.optDeclSig) fun x => HAndThen.hAndThen Lean.Parser.Command.declVal fun x => HAndThen.hAndThen Lean.Parser.Command.optDefDeriving fun x => Lean.Parser.Command.terminationSuffix))

source

def Lean.Parser.Command.theorem :

Lean.Parser.Parser

Equations

Lean.Parser.Command.theorem = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "theorem" (some `Lean.Parser.Command.theorem)) (Lean.Parser.leadingNode `Lean.Parser.Command.theorem 1024 (HAndThen.hAndThen (Lean.Parser.symbol "theorem ") fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.declSig) fun x => HAndThen.hAndThen Lean.Parser.Command.declVal fun x => Lean.Parser.Command.terminationSuffix))

source

def Lean.Parser.Command.constant :

Lean.Parser.Parser

Equations

Lean.Parser.Command.constant = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "constant" (some `Lean.Parser.Command.constant)) (Lean.Parser.leadingNode `Lean.Parser.Command.constant 1024 (HAndThen.hAndThen (Lean.Parser.symbol "constant ") fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.declSig) fun x => Lean.Parser.optional Lean.Parser.Command.declValSimple))

source

def Lean.Parser.Command.instance :

Lean.Parser.Parser

Equations

Lean.Parser.Command.instance = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "instance" (some `Lean.Parser.Command.instance)) (Lean.Parser.leadingNode `Lean.Parser.Command.instance 1024 (HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "instance") fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedPrio fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Command.declId)) fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.declSig) fun x => HAndThen.hAndThen Lean.Parser.Command.declVal fun x => Lean.Parser.Command.terminationSuffix))

source

def Lean.Parser.Command.axiom :

Lean.Parser.Parser

Equations

Lean.Parser.Command.axiom = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "axiom" (some `Lean.Parser.Command.axiom)) (Lean.Parser.leadingNode `Lean.Parser.Command.axiom 1024 (HAndThen.hAndThen (Lean.Parser.symbol "axiom ") fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => Lean.Parser.ppIndent Lean.Parser.Command.declSig))

source

def Lean.Parser.Command.example :

Lean.Parser.Parser

Equations

Lean.Parser.Command.example = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "example" (some `Lean.Parser.Command.example)) (Lean.Parser.leadingNode `Lean.Parser.Command.example 1024 (HAndThen.hAndThen (Lean.Parser.symbol "example") fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.declSig) fun x => Lean.Parser.Command.declVal))

source

def Lean.Parser.Command.inferMod :

Lean.Parser.Parser

Equations

Lean.Parser.Command.inferMod = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "inferMod" (some `Lean.Parser.Command.inferMod)) (Lean.Parser.leadingNode `Lean.Parser.Command.inferMod 1024 (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => Lean.Parser.symbol "}")))

source

def Lean.Parser.Command.ctor :

Lean.Parser.Parser

Equations

Lean.Parser.Command.ctor = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "ctor" (some `Lean.Parser.Command.ctor)) (Lean.Parser.leadingNode `Lean.Parser.Command.ctor 1024 (HAndThen.hAndThen (Lean.Parser.symbol "\n| ") fun x => Lean.Parser.ppIndent (HAndThen.hAndThen (Lean.Parser.Command.declModifiers true) fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.inferMod) fun x => Lean.Parser.Command.optDeclSig)))

source

def Lean.Parser.Command.derivingClasses :

Lean.Parser.Parser

Equations

Lean.Parser.Command.derivingClasses = Lean.Parser.sepBy1 (Lean.Parser.group (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " with ") fun x => Lean.Parser.Term.structInst))) ", " (Lean.Parser.symbol ", ")

source

def Lean.Parser.Command.optDeriving :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optDeriving = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "optDeriving" (some `Lean.Parser.Command.optDeriving)) (Lean.Parser.leadingNode `Lean.Parser.Command.optDeriving 1024 (Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "deriving ") fun x => Lean.Parser.notSymbol "instance")) fun x => Lean.Parser.Command.derivingClasses)))

source

def Lean.Parser.Command.inductive :

Lean.Parser.Parser

Equations

Lean.Parser.Command.inductive = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "inductive" (some `Lean.Parser.Command.inductive)) (Lean.Parser.leadingNode `Lean.Parser.Command.inductive 1024 (HAndThen.hAndThen (Lean.Parser.symbol "inductive ") fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen Lean.Parser.Command.optDeclSig fun x => HAndThen.hAndThen (Lean.Parser.optional (HOrElse.hOrElse (Lean.Parser.symbol " :=") fun x => Lean.Parser.symbol " where")) fun x => HAndThen.hAndThen (Lean.Parser.many Lean.Parser.Command.ctor) fun x => Lean.Parser.Command.optDeriving))

source

def Lean.Parser.Command.classInductive :

Lean.Parser.Parser

Equations

Lean.Parser.Command.classInductive = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "classInductive" (some `Lean.Parser.Command.classInductive)) (Lean.Parser.leadingNode `Lean.Parser.Command.classInductive 1024 (HAndThen.hAndThen (Lean.Parser.atomic (Lean.Parser.group (HAndThen.hAndThen (Lean.Parser.symbol "class ") fun x => Lean.Parser.symbol "inductive "))) fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.optDeclSig) fun x => HAndThen.hAndThen (Lean.Parser.optional (HOrElse.hOrElse (Lean.Parser.symbol " :=") fun x => Lean.Parser.symbol " where")) fun x => HAndThen.hAndThen (Lean.Parser.many Lean.Parser.Command.ctor) fun x => Lean.Parser.Command.optDeriving))

source

def Lean.Parser.Command.structExplicitBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structExplicitBinder = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structExplicitBinder" (some `Lean.Parser.Command.structExplicitBinder)) (Lean.Parser.leadingNode `Lean.Parser.Command.structExplicitBinder 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.Command.declModifiers true) fun x => Lean.Parser.symbol "(")) fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.ident) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.inferMod) fun x => HAndThen.hAndThen (Lean.Parser.ppIndent Lean.Parser.Command.optDeclSig) fun x => HAndThen.hAndThen (Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Term.binderTactic fun x => Lean.Parser.Term.binderDefault)) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Command.structImplicitBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structImplicitBinder = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structImplicitBinder" (some `Lean.Parser.Command.structImplicitBinder)) (Lean.Parser.leadingNode `Lean.Parser.Command.structImplicitBinder 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.Command.declModifiers true) fun x => Lean.Parser.symbol "{")) fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.ident) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.inferMod) fun x => HAndThen.hAndThen Lean.Parser.Command.declSig fun x => Lean.Parser.symbol "}"))

source

def Lean.Parser.Command.structInstBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structInstBinder = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structInstBinder" (some `Lean.Parser.Command.structInstBinder)) (Lean.Parser.leadingNode `Lean.Parser.Command.structInstBinder 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.Command.declModifiers true) fun x => Lean.Parser.symbol "[")) fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.ident) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.inferMod) fun x => HAndThen.hAndThen Lean.Parser.Command.declSig fun x => Lean.Parser.symbol "]"))

source

def Lean.Parser.Command.structSimpleBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structSimpleBinder = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structSimpleBinder" (some `Lean.Parser.Command.structSimpleBinder)) (Lean.Parser.leadingNode `Lean.Parser.Command.structSimpleBinder 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.Command.declModifiers true) fun x => Lean.Parser.ident)) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.inferMod) fun x => HAndThen.hAndThen Lean.Parser.Command.optDeclSig fun x => Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Term.binderTactic fun x => Lean.Parser.Term.binderDefault)))

source

def Lean.Parser.Command.declaration :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declaration = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "declaration" (some `Lean.Parser.Command.declaration)) (Lean.Parser.leadingNode `Lean.Parser.Command.declaration 1024 (HAndThen.hAndThen (Lean.Parser.Command.declModifiers false) fun x => HOrElse.hOrElse Lean.Parser.Command.abbrev fun x => HOrElse.hOrElse Lean.Parser.Command.def fun x => HOrElse.hOrElse Lean.Parser.Command.theorem fun x => HOrElse.hOrElse Lean.Parser.Command.constant fun x => HOrElse.hOrElse Lean.Parser.Command.instance fun x => HOrElse.hOrElse Lean.Parser.Command.axiom fun x => HOrElse.hOrElse Lean.Parser.Command.example fun x => HOrElse.hOrElse Lean.Parser.Command.inductive fun x => HOrElse.hOrElse Lean.Parser.Command.classInductive fun x => Lean.Parser.Command.structure))

source

def Lean.Parser.Command.structFields :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structFields = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structFields" (some `Lean.Parser.Command.structFields)) (Lean.Parser.leadingNode `Lean.Parser.Command.structFields 1024 (Lean.Parser.manyIndent (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen Lean.Parser.checkColGe fun x => Lean.Parser.ppGroup (HOrElse.hOrElse Lean.Parser.Command.structExplicitBinder fun x => HOrElse.hOrElse Lean.Parser.Command.structImplicitBinder fun x => HOrElse.hOrElse Lean.Parser.Command.structInstBinder fun x => Lean.Parser.Command.structSimpleBinder))))

source

def Lean.Parser.Command.structCtor :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structCtor = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structCtor" (some `Lean.Parser.Command.structCtor)) (Lean.Parser.leadingNode `Lean.Parser.Command.structCtor 1024 (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.Command.declModifiers true) fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.inferMod) fun x => Lean.Parser.symbol " :: ")))

source

def Lean.Parser.Command.structureTk :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structureTk = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structureTk" (some `Lean.Parser.Command.structureTk)) (Lean.Parser.leadingNode `Lean.Parser.Command.structureTk 1024 (Lean.Parser.symbol "structure "))

source

def Lean.Parser.Command.deriving :

Lean.Parser.Parser

Equations

Lean.Parser.Command.deriving = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "deriving" (some `Lean.Parser.Command.deriving)) (Lean.Parser.leadingNode `Lean.Parser.Command.deriving 1024 (HAndThen.hAndThen (Lean.Parser.symbol "deriving ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "instance ") fun x => HAndThen.hAndThen Lean.Parser.Command.derivingClasses fun x => HAndThen.hAndThen (Lean.Parser.symbol " for ") fun x => Lean.Parser.sepBy1 Lean.Parser.ident ", " (Lean.Parser.symbol ", ")))

source

def Lean.Parser.Command.classTk :

Lean.Parser.Parser

Equations

Lean.Parser.Command.classTk = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "classTk" (some `Lean.Parser.Command.classTk)) (Lean.Parser.leadingNode `Lean.Parser.Command.classTk 1024 (Lean.Parser.symbol "class "))

source

def Lean.Parser.Command.section :

Lean.Parser.Parser

Equations

Lean.Parser.Command.section = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "section" (some `Lean.Parser.Command.section)) (Lean.Parser.leadingNode `Lean.Parser.Command.section 1024 (HAndThen.hAndThen (Lean.Parser.symbol "section ") fun x => Lean.Parser.optional Lean.Parser.ident))

source

def Lean.Parser.Command.extends :

Lean.Parser.Parser

Equations

Lean.Parser.Command.extends = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "extends" (some `Lean.Parser.Command.extends)) (Lean.Parser.leadingNode `Lean.Parser.Command.extends 1024 (HAndThen.hAndThen (Lean.Parser.symbol " extends ") fun x => Lean.Parser.sepBy1 Lean.Parser.termParser ", " (Lean.Parser.symbol ", ")))

source

def Lean.Parser.Command.namespace :

Lean.Parser.Parser

Equations

Lean.Parser.Command.namespace = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "namespace" (some `Lean.Parser.Command.namespace)) (Lean.Parser.leadingNode `Lean.Parser.Command.namespace 1024 (HAndThen.hAndThen (Lean.Parser.symbol "namespace ") fun x => Lean.Parser.ident))

source

def Lean.Parser.Command.end :

Lean.Parser.Parser

Equations

Lean.Parser.Command.end = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "end" (some `Lean.Parser.Command.end)) (Lean.Parser.leadingNode `Lean.Parser.Command.end 1024 (HAndThen.hAndThen (Lean.Parser.symbol "end ") fun x => Lean.Parser.optional Lean.Parser.ident))

source

def Lean.Parser.Command.structure :

Lean.Parser.Parser

Equations

Lean.Parser.Command.structure = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structure" (some `Lean.Parser.Command.structure)) (Lean.Parser.leadingNode `Lean.Parser.Command.structure 1024 (HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.Command.structureTk fun x => Lean.Parser.Command.classTk) fun x => HAndThen.hAndThen Lean.Parser.Command.declId fun x => HAndThen.hAndThen (Lean.Parser.many (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.bracketedBinder)) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.extends) fun x => HAndThen.hAndThen Lean.Parser.Term.optType fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (HOrElse.hOrElse (Lean.Parser.symbol " := ") fun x => Lean.Parser.symbol " where ") fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.structCtor) fun x => Lean.Parser.Command.structFields)) fun x => Lean.Parser.Command.optDeriving))

source

def Lean.Parser.Command.variable :

Lean.Parser.Parser

Equations

Lean.Parser.Command.variable = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "variable" (some `Lean.Parser.Command.variable)) (Lean.Parser.leadingNode `Lean.Parser.Command.variable 1024 (HAndThen.hAndThen (Lean.Parser.symbol "variable") fun x => Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.bracketedBinder)))

source

def Lean.Parser.Command.universe :

Lean.Parser.Parser

Equations

Lean.Parser.Command.universe = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "universe" (some `Lean.Parser.Command.universe)) (Lean.Parser.leadingNode `Lean.Parser.Command.universe 1024 (HAndThen.hAndThen (Lean.Parser.symbol "universe ") fun x => Lean.Parser.many1 Lean.Parser.ident))

source

def Lean.Parser.Command.check :

Lean.Parser.Parser

Equations

Lean.Parser.Command.check = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "check" (some `Lean.Parser.Command.check)) (Lean.Parser.leadingNode `Lean.Parser.Command.check 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#check ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Command.noncomputableSection :

Lean.Parser.Parser

Equations

Lean.Parser.Command.noncomputableSection = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "noncomputableSection" (some `Lean.Parser.Command.noncomputableSection)) (Lean.Parser.leadingNode `Lean.Parser.Command.noncomputableSection 1024 (HAndThen.hAndThen (Lean.Parser.symbol "noncomputable ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "section ") fun x => Lean.Parser.optional Lean.Parser.ident))

source

def Lean.Parser.Command.check_failure :

Lean.Parser.Parser

Equations

Lean.Parser.Command.check_failure = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "check_failure" (some `Lean.Parser.Command.check_failure)) (Lean.Parser.leadingNode `Lean.Parser.Command.check_failure 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#check_failure ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Command.reduce :

Lean.Parser.Parser

Equations

Lean.Parser.Command.reduce = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "reduce" (some `Lean.Parser.Command.reduce)) (Lean.Parser.leadingNode `Lean.Parser.Command.reduce 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#reduce ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Command.eval :

Lean.Parser.Parser

Equations

Lean.Parser.Command.eval = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "eval" (some `Lean.Parser.Command.eval)) (Lean.Parser.leadingNode `Lean.Parser.Command.eval 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#eval ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Command.synth :

Lean.Parser.Parser

Equations

Lean.Parser.Command.synth = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "synth" (some `Lean.Parser.Command.synth)) (Lean.Parser.leadingNode `Lean.Parser.Command.synth 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#synth ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Command.exit :

Lean.Parser.Parser

Equations

Lean.Parser.Command.exit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "exit" (some `Lean.Parser.Command.exit)) (Lean.Parser.leadingNode `Lean.Parser.Command.exit 1024 (Lean.Parser.symbol "#exit"))

source

def Lean.Parser.Command.print :

Lean.Parser.Parser

Equations

Lean.Parser.Command.print = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "print" (some `Lean.Parser.Command.print)) (Lean.Parser.leadingNode `Lean.Parser.Command.print 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#print ") fun x => HOrElse.hOrElse Lean.Parser.ident fun x => Lean.Parser.strLit))

source

def Lean.Parser.Command.printAxioms :

Lean.Parser.Parser

Equations

Lean.Parser.Command.printAxioms = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "printAxioms" (some `Lean.Parser.Command.printAxioms)) (Lean.Parser.leadingNode `Lean.Parser.Command.printAxioms 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#print ") fun x => HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "axioms ") fun x => Lean.Parser.ident))

source

def Lean.Parser.Command.resolve_name :

Lean.Parser.Parser

Equations

Lean.Parser.Command.resolve_name = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "resolve_name" (some `Lean.Parser.Command.resolve_name)) (Lean.Parser.leadingNode `Lean.Parser.Command.resolve_name 1024 (HAndThen.hAndThen (Lean.Parser.symbol "#resolve_name ") fun x => Lean.Parser.ident))

source

def Lean.Parser.Command.init_quot :

Lean.Parser.Parser

Equations

Lean.Parser.Command.init_quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "init_quot" (some `Lean.Parser.Command.init_quot)) (Lean.Parser.leadingNode `Lean.Parser.Command.init_quot 1024 (Lean.Parser.symbol "init_quot"))

source

def Lean.Parser.Command.set_option :

Lean.Parser.Parser

Equations

Lean.Parser.Command.set_option = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "set_option" (some `Lean.Parser.Command.set_option)) (Lean.Parser.leadingNode `Lean.Parser.Command.set_option 1024 (HAndThen.hAndThen (Lean.Parser.symbol "set_option ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Command.optionValue))

source

def Lean.Parser.Command.attribute :

Lean.Parser.Parser

Equations

Lean.Parser.Command.attribute = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "attribute" (some `Lean.Parser.Command.attribute)) (Lean.Parser.leadingNode `Lean.Parser.Command.attribute 1024 (HAndThen.hAndThen (Lean.Parser.symbol "attribute ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "[") fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 (HOrElse.hOrElse Lean.Parser.Command.eraseAttr fun x => Lean.Parser.Term.attrInstance) ", " (Lean.Parser.symbol ", ")) fun x => HAndThen.hAndThen (Lean.Parser.symbol "] ") fun x => Lean.Parser.many1 Lean.Parser.ident))

source

def Lean.Parser.Command.export :

Lean.Parser.Parser

Equations

Lean.Parser.Command.export = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "export" (some `Lean.Parser.Command.export)) (Lean.Parser.leadingNode `Lean.Parser.Command.export 1024 (HAndThen.hAndThen (Lean.Parser.symbol "export ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol " (") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.ident) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Command.optionValue :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optionValue = HOrElse.hOrElse (Lean.Parser.nonReservedSymbol "true") fun x => HOrElse.hOrElse (Lean.Parser.nonReservedSymbol "false") fun x => HOrElse.hOrElse Lean.Parser.strLit fun x => Lean.Parser.numLit

source

def Lean.Parser.Command.open :

Lean.Parser.Parser

Equations

Lean.Parser.Command.open = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "open" (some `Lean.Parser.Command.open)) (Lean.Parser.leadingNode `Lean.Parser.Command.open 1024 (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "open ") fun x => Lean.Parser.Command.openDecl)))

source

def Lean.Parser.Command.eraseAttr :

Lean.Parser.Parser

Equations

Lean.Parser.Command.eraseAttr = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "eraseAttr" (some `Lean.Parser.Command.eraseAttr)) (Lean.Parser.leadingNode `Lean.Parser.Command.eraseAttr 1024 (HAndThen.hAndThen (Lean.Parser.symbol "-") fun x => Lean.Parser.rawIdent))

source

def Lean.Parser.Command.mutual :

Lean.Parser.Parser

Equations

Lean.Parser.Command.mutual = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "mutual" (some `Lean.Parser.Command.mutual)) (Lean.Parser.leadingNode `Lean.Parser.Command.mutual 1024 (HAndThen.hAndThen (Lean.Parser.symbol "mutual ") fun x => HAndThen.hAndThen (Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen (Lean.Parser.notSymbol "end") fun x => Lean.Parser.commandParser)) fun x => HAndThen.hAndThen (Lean.Parser.ppDedent (HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.symbol "end")) fun x => Lean.Parser.Command.terminationSuffix))

source

def Lean.Parser.Command.openHiding :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openHiding = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "openHiding" (some `Lean.Parser.Command.openHiding)) (Lean.Parser.leadingNode `Lean.Parser.Command.openHiding 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.symbol "hiding")) fun x => Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.checkColGt fun x => Lean.Parser.ident)))

source

def Lean.Parser.Command.initialize :

Lean.Parser.Parser

Equations

Lean.Parser.Command.initialize = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "initialize" (some `Lean.Parser.Command.initialize)) (Lean.Parser.leadingNode `Lean.Parser.Command.initialize 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.visibility) fun x => HAndThen.hAndThen (Lean.Parser.symbol "initialize ") fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen Lean.Parser.Term.typeSpec fun x => Lean.Parser.Term.leftArrow))) fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Command.openRenamingItem :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openRenamingItem = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "openRenamingItem" (some `Lean.Parser.Command.openRenamingItem)) (Lean.Parser.leadingNode `Lean.Parser.Command.openRenamingItem 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen (Lean.Parser.unicodeSymbol " → " " -> ") fun x => HAndThen.hAndThen Lean.Parser.checkColGt fun x => Lean.Parser.ident))

source

def Lean.Parser.Command.builtin_initialize :

Lean.Parser.Parser

Equations

Lean.Parser.Command.builtin_initialize = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "builtin_initialize" (some `Lean.Parser.Command.builtin_initialize)) (Lean.Parser.leadingNode `Lean.Parser.Command.builtin_initialize 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.visibility) fun x => HAndThen.hAndThen (Lean.Parser.symbol "builtin_initialize ") fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen Lean.Parser.Term.typeSpec fun x => Lean.Parser.Term.leftArrow))) fun x => Lean.Parser.Term.doSeq))

source

def Lean.Parser.Command.openRenaming :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openRenaming = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "openRenaming" (some `Lean.Parser.Command.openRenaming)) (Lean.Parser.leadingNode `Lean.Parser.Command.openRenaming 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.symbol "renaming")) fun x => Lean.Parser.sepBy1 Lean.Parser.Command.openRenamingItem ", " (Lean.Parser.symbol ", ")))

source

def Lean.Parser.Command.in :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Command.in = Lean.Parser.trailingNode `Lean.Parser.Command.in 1024 0 (Lean.Parser.withOpen (HAndThen.hAndThen (Lean.Parser.symbol " in ") fun x => Lean.Parser.commandParser))

source

def Lean.Parser.Command.openOnly :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openOnly = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "openOnly" (some `Lean.Parser.Command.openOnly)) (Lean.Parser.leadingNode `Lean.Parser.Command.openOnly 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.symbol " (")) fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.ident) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Command.openSimple :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openSimple = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "openSimple" (some `Lean.Parser.Command.openSimple)) (Lean.Parser.leadingNode `Lean.Parser.Command.openSimple 1024 (Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.checkColGt fun x => Lean.Parser.ident)))

source

def Lean.Parser.Command.openScoped :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openScoped = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "openScoped" (some `Lean.Parser.Command.openScoped)) (Lean.Parser.leadingNode `Lean.Parser.Command.openScoped 1024 (HAndThen.hAndThen (Lean.Parser.symbol "scoped ") fun x => Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.checkColGt fun x => Lean.Parser.ident)))

source

def Lean.Parser.Command.openDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Command.openDecl = HOrElse.hOrElse Lean.Parser.Command.openHiding fun x => HOrElse.hOrElse Lean.Parser.Command.openRenaming fun x => HOrElse.hOrElse Lean.Parser.Command.openOnly fun x => HOrElse.hOrElse Lean.Parser.Command.openSimple fun x => Lean.Parser.Command.openScoped

source

def Lean.Parser.Command.genInjectiveTheorems :

Lean.Parser.Parser

Equations

Lean.Parser.Command.genInjectiveTheorems = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "genInjectiveTheorems" (some `Lean.Parser.Command.genInjectiveTheorems)) (Lean.Parser.leadingNode `Lean.Parser.Command.genInjectiveTheorems 1024 (HAndThen.hAndThen (Lean.Parser.symbol "gen_injective_theorems% ") fun x => Lean.Parser.ident))

source

@[inline]

abbrev Lean.Parser.Command.declModifiersF :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declModifiersF = Lean.Parser.Command.declModifiers false

source

@[inline]

abbrev Lean.Parser.Command.declModifiersT :

Lean.Parser.Parser

Equations

Lean.Parser.Command.declModifiersT = Lean.Parser.Command.declModifiers true

source

def Lean.Parser.Term.open :

Lean.Parser.Parser

Equations

Lean.Parser.Term.open = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "open" (some `Lean.Parser.Term.open)) (Lean.Parser.leadingNode `Lean.Parser.Term.open Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "open ") fun x => HAndThen.hAndThen Lean.Parser.Command.openDecl fun x => Lean.Parser.withOpenDecl (HAndThen.hAndThen (Lean.Parser.symbol " in ") fun x => Lean.Parser.termParser)))

source

def Lean.Parser.Term.set_option :

Lean.Parser.Parser

Equations

Lean.Parser.Term.set_option = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "set_option" (some `Lean.Parser.Term.set_option)) (Lean.Parser.leadingNode `Lean.Parser.Term.set_option Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "set_option ") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen Lean.Parser.Command.optionValue fun x => HAndThen.hAndThen (Lean.Parser.symbol " in ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Tactic.open :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.open = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "open" (some `Lean.Parser.Tactic.open)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.open Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "open ") fun x => HAndThen.hAndThen Lean.Parser.Command.openDecl fun x => Lean.Parser.withOpenDecl (HAndThen.hAndThen (Lean.Parser.symbol " in ") fun x => Lean.Parser.Tactic.tacticSeq)))

source

def Lean.Parser.Tactic.set_option :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.set_option = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "set_option" (some `Lean.Parser.Tactic.set_option)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.set_option Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "set_option ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen Lean.Parser.Command.optionValue fun x => HAndThen.hAndThen (Lean.Parser.symbol " in ") fun x => Lean.Parser.Tactic.tacticSeq))