Bound the depth of hole searching
In case the only infinite part of a term is in an implicit argument.
commit914d99235916ced3bd2ed3e2ba8fa3f5b18d7a45
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateMon 2 Feb 2015, 01:32 (12 years ago)
parentb8abab8
src/Idris/AbsSyntaxTree.hs+1−1
@@ -1650,7 +1650,7 @@ isHoleName _ = False
16501650
16511651-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
16521652containsHole :: PTerm -> Bool
1653−containsHole pterm = or [isHoleName n | PRef _ n <- universe pterm]
1653+containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]
16541654
16551655-- | Pretty-printer helper for the binding site of a name
16561656bindingOf :: Name -- ^^ the bound name