Documentation

Lean.Parser.Term

source
def Lean.Parser.Command.commentBody:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Command.commentBody.parenthesizer:
Lean.PrettyPrinter.Parenthesizer
Equations
source
def Lean.Parser.Command.commentBody.formatter:
Lean.PrettyPrinter.Formatter
Equations
source
def Lean.Parser.Command.docComment:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
def Lean.Parser.tacticParser (rbp : optParam Nat 0) :
Lean.Parser.Parser
Equations
source
@[inline]
def Lean.Parser.convParser (rbp : optParam Nat 0) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.Tactic.tacticSeq1Indented:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.tacticSeqBracketed:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.tacticSeq:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.seq1:
Lean.Parser.Parser
Equations
source
def Lean.Parser.darrow:
Lean.Parser.Parser
Equations
source
def Lean.Parser.semicolonOrLinebreak:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.byTactic:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.byTactic':
Lean.Parser.Parser

This is the same as byTactic, but it uses a different syntax kind. This is used by show and suffices instead of byTactic because these syntaxes don't support arbitrary terms where byTactic is accepted. Mathport uses this to e.g. safely find-replace by exact $e by $e in any context without causing incorrect syntax when the full expression is show $T by exact $e.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.optSemicolon (p : Lean.Parser.Parser) :
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.ident:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.num:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.scientific:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.str:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.char:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.type:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.sort:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.prop:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.hole:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.syntheticHole:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.sorry:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.cdot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.typeAscription:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.tupleTail:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.parenSpecial:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.paren:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.anonymousCtor:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.optIdent:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.fromTerm:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.showRhs:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.sufficesDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.suffices:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.show:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.structInstArrayRef:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.structInstLVal:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.structInstField:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.structInstFieldAbbrev:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.optEllipsis:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.structInst:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.typeSpec:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.optType:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.explicit:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.inaccessible:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binderIdent:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.binderType (requireType : optParam Bool false) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binderTactic:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binderDefault:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.explicitBinder (requireType : optParam Bool false) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.implicitBinder (requireType : optParam Bool false) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.strictImplicitLeftBracket:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.strictImplicitRightBracket:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.strictImplicitBinder (requireType : optParam Bool false) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.instBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.bracketedBinder (requireType : optParam Bool false) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.depArrow:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.simpleBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.forall:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.matchAlt (rhsParser : optParam Lean.Parser.Parser Lean.Parser.termParser) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.matchAltExpr:
Lean.Parser.Parser

Useful for syntax quotations. Note that generic patterns such as `(matchAltExpr| | ... => $rhs) should also work with other rhsParsers (of arity 1).

Equations
source
instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStrAnonymousNil:
Coe (Lean.TSyntax `Lean.Parser.Term.matchAltExpr) (Lean.TSyntax `Lean.Parser.Term.matchAlt)
Equations
source
def Lean.Parser.Term.matchAlts (rhsParser : optParam Lean.Parser.Parser Lean.Parser.termParser) :
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.matchDiscr:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.trueVal:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.falseVal:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.generalizingParam:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.motive:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.match:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.nomatch:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.funImplicitBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.funStrictImplicitBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.funSimpleBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.funBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.basicFun:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.fun:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.optExprPrecedence:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.withAnonymousAntiquot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.leading_parser:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.trailing_parser:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.borrowed:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.quotedName:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.doubleQuotedName:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.simpleBinderWithoutType:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letIdBinder:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letIdLhs:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letIdDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letPatDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letEqnsDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.let:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.let_fun:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.let_delayed:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.let_tmp:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
instance Lean.Parser.Term.instCoeTSyntaxConsSyntaxNodeKindMkStrAnonymousNil_1:
Coe (Lean.TSyntax `Lean.Parser.Term.letIdBinder) (Lean.TSyntax `Lean.Parser.Term.funBinder)
Equations
source
def Lean.Parser.Term.haveIdLhs:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.haveIdDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.haveEqnsDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.haveDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.have:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.scoped:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.local:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.attrKind:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.attrInstance:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.attributes:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letRecDecl:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letRecDecls:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letrec:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.whereDecls:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.matchAltsWhereDecls:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.noindex:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binrel:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binrel_no_prop:
Lean.Parser.Parser

Similar to binrel, but coerse Prop arguments into Bool.

Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binop:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.binop_lazy:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.forInMacro:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.forInMacro':
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.typeOf:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.ensureTypeOf:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.ensureExpectedType:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.noImplicitLambda:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.letMVar:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.waitIfTypeMVar:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.waitIfTypeContainsMVar:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.waitIfContainsMVar:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.defaultOrOfNonempty:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.namedArgument:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.ellipsis:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.argument:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.app:
Lean.Parser.TrailingParser
Equations
source
def Lean.Parser.Term.proj:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.completion:
Lean.Parser.TrailingParser
Equations
source
def Lean.Parser.Term.arrayRef:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.arrow:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.isIdent (stx : Lean.Syntax) :
Bool
Equations
source
def Lean.Parser.Term.explicitUniv:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.namedPattern:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.pipeProj:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.pipeCompletion:
Lean.Parser.TrailingParser
Equations
source
def Lean.Parser.Term.subst:
Lean.Parser.TrailingParser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.funBinder.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.bracketedBinderF:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.bracketedBinder.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.matchDiscr.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.attr.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.panic:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.unreachable:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.dbgTrace:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.assert:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.macroArg:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.macroDollarArg:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.macroLastArg:
Lean.Parser.Parser
Equations
source
def Lean.Parser.Term.stateRefT:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.dynamicQuot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Term.dotIdent:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Tactic.quotSeq:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Parser.Level.quot:
Lean.Parser.Parser
Equations
  • One or more equations did not get rendered due to their size.