@@ -245,7 +245,7 @@ replaceSplits :: String -> [[(Name, PTerm)]] -> Idris [String]
245replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
245replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
247 rep str [] = str ++ "\n"
247 rep str [] = str ++ "\n"
248− rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow False tm) str) ups
248+ rep str ((n, tm) : ups) = rep (updatePat False (show n) (nshow tm) str) ups
250 updateRHSs i [] = return []
250 updateRHSs i [] = return []
251 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
251 updateRHSs i (x : xs) = do (x', i') <- updateRHS i x
@@ -264,11 +264,10 @@ replaceSplits l ups = updateRHSs 1 (map (rep (expandBraces l)) ups)
265 -- TMP HACK: If there are Nats, we don't want to show as numerals since
265 -- TMP HACK: If there are Nats, we don't want to show as numerals since
266 -- this isn't supported in a pattern, so special case here
266 -- this isn't supported in a pattern, so special case here
267− nshow brack (PRef _ (UN "Z")) = "Z"
267+ nshow (PRef _ (UN "Z")) = "Z"
268− nshow brack (PApp _ (PRef _ (UN "S")) [x]) =
268+ nshow (PApp _ (PRef _ (UN "S")) [x]) =
269− if brack then "(S " else "S " ++ nshow True (getTm x) ++
269+ "S " ++ addBrackets (nshow (getTm x))
270− if brack then ")" else ""
271− nshow _ t = show t
270+ nshow t = show t
273 -- if there's any {n} replace with {n=n}
272 -- if there's any {n} replace with {n=n}
274 expandBraces ('{' : xs)
273 expandBraces ('{' : xs)