46f734b1b1
Also make sure that the name inside a node kind is the full name of the declaration. This way, we cannot have accidentally conflicting node kind names.
28 lines
571 B
Text
28 lines
571 B
Text
/-
|
|
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Author: Sebastian Ullrich
|
|
|
|
Term-level readers and macros
|
|
-/
|
|
prelude
|
|
import init.lean.parser.reader.token
|
|
|
|
namespace lean.parser
|
|
namespace reader
|
|
open combinators
|
|
|
|
@[pattern] def hole := {syntax_node_kind . name := `lean.parser.reader.hole}
|
|
|
|
@[derive reader.has_tokens]
|
|
def hole.reader : reader :=
|
|
node hole [symbol "_"]
|
|
|
|
@[derive reader.has_tokens reader.has_view]
|
|
def term.reader :=
|
|
any_of [
|
|
hole.reader
|
|
]
|
|
|
|
end reader
|
|
end lean.parser
|