From f955552d5bb34452dcd9779acc821a2a65150426 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 12 Aug 2020 14:07:23 -0700
Subject: [PATCH] feat: elaborate `.(t)`

---
 src/Lean/Elab/Match.lean | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index c1dc72b2ba..1b4f2b192e 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -92,6 +92,15 @@ private def getMatchAlts (stx : Syntax) : Array MatchAltView :=
 let alts : Array Syntax := (stx.getArg 5).getArgs.filter fun alt => alt.getKind == `Lean.Parser.Term.matchAlt;
 alts.map mkMatchAltView
 
+/--
+  Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
+  `_` in patterns. -/
+def mkInaccessible (e : Expr) : Expr :=
+mkAnnotation `_inaccessible e
+
+def isInaccessible? (e : Expr) : Option Expr :=
+isAnnotation? `_inaccessible e
+
 inductive PatternVar
 | localVar     (userName : Name)
 -- anonymous variables (`_`) are encoded using metavariables
@@ -121,7 +130,12 @@ private def getMVarSyntaxMVarId (stx : Syntax) : MVarId :=
   The elaboration function for `Syntax` created using `mkMVarSyntax`.
   It just converts the metavariable id wrapped by the Syntax into an `Expr`. -/
 @[builtinTermElab MVarWithIdKind] def elabMVarWithIdKind : TermElab :=
-fun stx expectedType? => pure $ mkMVar (getMVarSyntaxMVarId stx)
+fun stx expectedType? => pure $ mkInaccessible $ mkMVar (getMVarSyntaxMVarId stx)
+
+@[builtinTermElab inaccessible] def elabInaccessible : TermElab :=
+fun stx expectedType? => do
+  e ← elabTerm (stx.getArg 1) expectedType?;
+  pure $ mkInaccessible e
 
 /-
   Patterns define new local variables.