From 218af640bbc243a4f9ddff45add862d396c85635 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Fri, 20 Jul 2018 18:44:37 +0200
Subject: [PATCH] fix(library/init/lean/parser/reader/term): add missing file

---
 library/init/lean/parser/reader/term.lean | 26 +++++++++++++++++++++++
 1 file changed, 26 insertions(+)
 create mode 100644 library/init/lean/parser/reader/term.lean

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