diff --git a/library/init/lean/parser/reader/term.lean b/library/init/lean/parser/reader/term.lean new file mode 100644 index 0000000000..234798cee4 --- /dev/null +++ b/library/init/lean/parser/reader/term.lean @@ -0,0 +1,26 @@ +/- +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 + +def hole := {macro . name := `hole} + +def hole.reader : reader := +node hole [symbol "_"] + +def term.reader := +any_of [ + hole.reader +] + +end reader +end lean.parser