diff --git a/src/TTImp/Elab/App.idr b/src/TTImp/Elab/App.idr index 066c729b8..0b9f8578c 100644 --- a/src/TTImp/Elab/App.idr +++ b/src/TTImp/Elab/App.idr @@ -836,12 +836,13 @@ checkApp rig elabinfo nest env fc (IVar fc' n) expargs autoargs namedargs exp boundSafe : Constant -> ElabMode -> Bool boundSafe _ (InLHS _) = True -- always need to expand on LHS - boundSafe (BI x) _ = abs x < 100 -- only do this for relatively small bounds. - -- Once it gets too big, we might be making the term - -- bigger than it would have been without evaluating! + -- only do this for relatively small bounds. + -- Once it gets too big, we might be making the term + -- bigger than it would have been without evaluating! + boundSafe (BI x) _ = abs x < 100 + boundSafe (Str str) _ = length str < 10 boundSafe _ _ = True - updateElabInfo : List Name -> ElabMode -> Name -> List RawImp -> ElabInfo -> Core ElabInfo -- If it's a primitive function applied to a constant on the LHS, treat it