非結合中置演算子は Lean.Parser.Command.mixfix : command
infix
で定義されます:
command ::= ... |docComment? attributes?
A
docComment
parses a "documentation comment" like/-- foo -/
. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.A
docComment
node contains a/--
atom and then the remainder of the comment,foo -/
in this example. UseTSyntax.getDocString
to extract the body text from a doc string syntax node.attrKind infix:prec ((name := ident))? ((priority := prio))? str => term
attrKind
matches("scoped" <|> "local")?
, used before an attribute like@[local simp]
.
左結合中置演算子は Lean.Parser.Command.mixfix : command
infixl
で定義されます:
command ::= ... |docComment? attributes?
A
docComment
parses a "documentation comment" like/-- foo -/
. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.A
docComment
node contains a/--
atom and then the remainder of the comment,foo -/
in this example. UseTSyntax.getDocString
to extract the body text from a doc string syntax node.attrKind infixl:prec ((name := ident))? ((priority := prio))? str => term
attrKind
matches("scoped" <|> "local")?
, used before an attribute like@[local simp]
.
右結合中置演算子は Lean.Parser.Command.mixfix : command
infixr
で定義されます:
command ::= ... |docComment? attributes?
A
docComment
parses a "documentation comment" like/-- foo -/
. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.A
docComment
node contains a/--
atom and then the remainder of the comment,foo -/
in this example. UseTSyntax.getDocString
to extract the body text from a doc string syntax node.attrKind infixr:prec ((name := ident))? ((priority := prio))? str => term
attrKind
matches("scoped" <|> "local")?
, used before an attribute like@[local simp]
.
前置演算子は Lean.Parser.Command.mixfix : command
prefix
で定義されます:
command ::= ... |docComment? attributes?
A
docComment
parses a "documentation comment" like/-- foo -/
. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.A
docComment
node contains a/--
atom and then the remainder of the comment,foo -/
in this example. UseTSyntax.getDocString
to extract the body text from a doc string syntax node.attrKind prefix:prec ((name := ident))? ((priority := prio))? str => term
attrKind
matches("scoped" <|> "local")?
, used before an attribute like@[local simp]
.
後置演算子は Lean.Parser.Command.mixfix : command
postfix
で定義されます:
command ::= ... |docComment? attributes?
A
docComment
parses a "documentation comment" like/-- foo -/
. This is not treated like a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.A
docComment
node contains a/--
atom and then the remainder of the comment,foo -/
in this example. UseTSyntax.getDocString
to extract the body text from a doc string syntax node.attrKind postfix:prec ((name := ident))? ((priority := prio))? str => term
attrKind
matches("scoped" <|> "local")?
, used before an attribute like@[local simp]
.