@@ -1016,6 +1016,7 @@ showImp impl tm = se 10 tm where
1016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1016 = bracket p 2 $ "{tacimp " ++ show n ++ " : " ++ se 10 ty ++ "} -> " ++ se 10 sc
1018 | Just str <- slist p e = str
1018 | Just str <- slist p e = str
1019+ | Just num <- snat p e = show num
1019 se p (PApp _ (PRef _ f) [])
1020 se p (PApp _ (PRef _ f) [])
1020 | not impl = show f
1021 | not impl = show f
1021 se p (PApp _ (PRef _ op@(UN (f:_))) args)
1022 se p (PApp _ (PRef _ op@(UN (f:_))) args)
@@ -1073,6 +1074,18 @@ showImp impl tm = se 10 tm where
1073 xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1074 xs -> "[" ++ intercalate "," (map (se p) xs) ++ "]"
1074 slist _ _ = Nothing
1075 slist _ _ = Nothing
1077+ -- since Prelude is always imported, S & O are unqualified iff they're the
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
1087+ natns = "Prelude.Nat."
1076 sArg (PImp _ _ n tm _) = siArg (n, tm)
1089 sArg (PImp _ _ n tm _) = siArg (n, tm)
1077 sArg (PExp _ _ tm _) = seArg tm
1090 sArg (PExp _ _ tm _) = seArg tm
1078 sArg (PConstraint _ _ tm _) = scArg tm
1091 sArg (PConstraint _ _ tm _) = scArg tm