manyIndent

Stream: lean4

[Mac]

Why does the manyIndent parser not work in syntax?

import Lean.Parser
open Lean Parser

#check manyIndent -- manyIndent : Parser → Parser
syntax foo := manyIndent(group(term ","?)) -- Error: parser 'manyIndent' was not found

[Sebastian Ullrich]

short answer: Parser combinators cannot be used directly, they must be registered via register_parser_alias. But I suppose all ingredients to reimplement it are exposed.

[Mac]

@Sebastian Ullrich Could we get parser aliases for manyIndent/many1Indent in core? They seem quite useful for DSLs that want custom do or structure like syntax.

[Mac]

While,, as you mentioned, they can be replicated in downstream code already, that seems like somewhat unnecessary code duplication.

[Sebastian Ullrich]

done