feat(library/init/lean/parser/syntax): Syntax.hasMissing

leanprover · Apr 1, 2019 · 89a607d · 89a607d
1 parent fc20c1f
commit 89a607d
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/library/init/lean/parser/syntax.lean b/library/init/lean/parser/syntax.lean
@@ -186,6 +186,11 @@ def getPos (stx : Syntax) : Option Parsec.Position :=
 do i ← stx.getHeadInfo,
    pure i.pos
 
+partial def hasMissing : Syntax → Bool
+| missing     := true
+| (rawNode n) := n.args.foldl (λ s r, hasMissing s || r) false
+| _           := false
+
 def reprintAtom : SyntaxAtom → String
 | ⟨some info, s⟩ := info.leading.toString ++ s ++ info.trailing.toString
 | ⟨none, s⟩      := s