filter out definitions with holes when trying examples

frontend/src/Language/Granule/Syntax/Def.hs

@@ -262,11 +262,15 @@ instance Monad m => Freshenable m (Def v a) where
 instance Term (EquationList v a) where
   freeVars (EquationList _ name _ eqs) =
     delete name (concatMap freeVars eqs)
+  hasHole (EquationList _ name _ eqs) = any hasHole eqs
 
 instance Term (Equation v a) where
   freeVars (Equation s _ a _ binders body) =
       freeVars body \\ concatMap boundVars binders
+  hasHole (Equation _ _ _ _ _ body) = hasHole body
 
 instance Term (Def v a) where
   freeVars (Def _ name _ _ equations _) =
     delete name (freeVars equations)
+  hasHole (Def _ name _ _ equations _) =
+    hasHole equations

frontend/src/Language/Granule/Synthesis/Synth.hs

@@ -16,6 +16,7 @@ import Language.Granule.Syntax.Expr
 import Language.Granule.Syntax.Type
 import Language.Granule.Syntax.Identifiers
 -- import Control.Monad.Logic
+import Language.Granule.Syntax.Helpers hiding (freshIdentifierBase)
 import Language.Granule.Syntax.Pretty
 import Language.Granule.Syntax.Pattern
 import Language.Granule.Syntax.Span
@@ -513,7 +514,11 @@ runExamples eval ast@(AST decls defs imports hidden mod) examples defId = do
           map (\(Example input output _) -> makeEquality input output) examples'
     -- remove the existing main function (should probably keep the main function so we can stitch it back in after)
 
-    let defsWithoutMain = filter (\(Def _ mIdent _ _ _ _) -> mIdent /= mkId entryPoint) defs
+    let defsWithoutMain =
+         filter (\(Def _ mIdent _ _ defs _) ->
+                       mIdent /= mkId entryPoint
+                       -- filter out any definitions that have a hole
+                    && not (hasHole defs)) defs
 
     let foundBoolDecl = find (\(DataDecl _ dIdent _ _ _) ->  dIdent == mkId "Bool") decls
     let declsWithBool = case foundBoolDecl of