Expand optional «precedence» where
«precedence» := leading_parser " : " >> precedenceParser
Instances For
- catName : Lake.Name
- first : Bool
- leftRec : Bool
- behavior : Lean.Parser.LeadingIdentBehavior
See comment at
Parser.ParserCategory.
Instances For
(Try to) add a term info for the category catName at ref.
Instances For
(Try to) add a term info for the alias with info info at ref.
Instances For
Instances For
Instances For
Instances For
Given a stx of category syntax, return a (newStx, lhsPrec?),
where newStx is of category term. After elaboration, newStx should have type
TrailingParserDescr if lhsPrec?.isSome, and ParserDescr otherwise.
Instances For
Sequence (aka NullNode)
Instances For
Instances For
Instances For
Instances For
Auxiliary function for creating declaration names from parser descriptions. Example: Given
syntax term "+" term : term
syntax "[" sepBy(term, ", ") "]" : term
It generates the names term_+_ and term[_,]
Instances For
Instances For
Instances For
Add macro scope to name if it does not already have them, and attrKind is local.
Instances For
Instances For
Instances For
Infer syntax kind k from first pattern, put alternatives of same kind into new macro/elab_rules (kind := k) via mkCmd (some k),
leave remaining alternatives (via mkCmd none) to be recursively expanded.