From b24796d98efcbcade599d121df6e99392192c853 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sun, 20 Jan 2019 16:41:33 +0100
Subject: [PATCH] feat(library/init/lean/elaborator): inaccessible

---
 library/init/lean/elaborator.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 52fb359eb6..c6cc587cf6 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -271,6 +271,9 @@ def to_pexpr : syntax → elaborator_m expr
     | explicit_modifier.view.explicit _         := `@
     | explicit_modifier.view.partial_explicit _ := `@@,
     expr.mk_annotation ann <$> to_pexpr (review ident_univs v.id)
+  | @inaccessible := do
+    let v := view inaccessible stx,
+    expr.mk_annotation `innaccessible <$> to_pexpr v.term  -- sic
   | @number := do
     let v := view number stx,
     pure $ expr.lit $ literal.nat_val v.to_nat