git.iko.soy/Idris-dev
on master help sign in
Bound the depth of hole searching
914d992David Raymond Christiansen
src/Idris/AbsSyntaxTree.hs+1−1
compare with master
unifiedsplit
@@ -1650,7 +1650,7 @@ isHoleName _ = False
1650
1650
1651-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1651-- | Check whether a PTerm has been delaborated from a Term containing a Hole or Guess
1652containsHole :: PTerm -> Bool
1652containsHole :: PTerm -> Bool
1653−containsHole pterm = or [isHoleName n | PRef _ n <- universe pterm]
1653+containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]
1654
1654
1655-- | Pretty-printer helper for the binding site of a name
1655-- | Pretty-printer helper for the binding site of a name
1656bindingOf :: Name -- ^^ the bound name
1656bindingOf :: Name -- ^^ the bound name