diff --git a/src/Init/Lean/Data/KVMap.lean b/src/Init/Lean/Data/KVMap.lean
index e1abed5267..8b0623cac4 100644
--- a/src/Init/Lean/Data/KVMap.lean
+++ b/src/Init/Lean/Data/KVMap.lean
@@ -65,6 +65,9 @@ def empty : KVMap :=
 def isEmpty : KVMap → Bool
 | ⟨m⟩ => m.isEmpty
 
+def size (m : KVMap) : Nat :=
+m.entries.length
+
 def findCore : List (Name × DataValue) → Name → Option DataValue
 | [],       k' => none
 | (k,v)::m, k' => if k == k' then some v else findCore m k'
diff --git a/src/Init/Lean/Expr.lean b/src/Init/Lean/Expr.lean
index a5ef75052b..f8b4d33ca6 100644
--- a/src/Init/Lean/Expr.lean
+++ b/src/Init/Lean/Expr.lean
@@ -905,5 +905,13 @@ private partial def getParamSubstArray (ps : Array Name) (us : Array Level) (p'
 def instantiateLevelParamsArray (e : Expr) (paramNames : Array Name) (lvls : Array Level) : Expr :=
 instantiateLevelParamsCore (fun p => getParamSubstArray paramNames lvls p 0) e
 
+def mkAnnotation (kind : Name) (e : Expr) : Expr :=
+mkMData (KVMap.empty.insert kind (DataValue.ofBool true)) e
+
+def isAnnotation? (kind : Name) (e : Expr) : Option Expr :=
+match e with
+| Expr.mdata d e _ => if d.size == 1 && d.getBool kind false then some e else none
+| _                => none
+
 end Expr
 end Lean