@@ -1016,6 +1016,7 @@ showImp impl tm = se 10 tm where
10161016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
10171017 se p e
10181018 | Just str <- slist p e = str
1019+ | Just num <- snat p e = show num
10191020 se p (PApp _ (PRef _ f) [])
10201021 | not impl = show f
10211022 se p (PApp _ (PRef _ op@(UN (f:_))) args)
@@ -1073,6 +1074,18 @@ showImp impl tm = se 10 tm where
10731074 xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
10741075 slist _ _ = Nothing
10751076
1077+ -- since Prelude is always imported, S & O are unqualified iff they're the
1078+ -- Nat ones.
1079+ snat p (PRef _ o)
1080+ | show o == (natns++"O") || show o == "O" = Just 0
1081+ snat p (PApp _ s [PExp {getTm=n}])
1082+ | show s == (natns++"S") || show s == "S",
1083+ Just n' <- snat p n
1084+ = Just $ 1 + n'
1085+ snat _ _ = Nothing
1086+
1087+ natns = "Prelude.Nat."
1088+
10761089 sArg (PImp _ _ n tm _) = siArg (n, tm)
10771090 sArg (PExp _ _ tm _) = seArg tm
10781091 sArg (PConstraint _ _ tm _) = scArg tm