diff --git a/lib/Quox/Equal.idr b/lib/Quox/Equal.idr index 789b49c..5998b3d 100644 --- a/lib/Quox/Equal.idr +++ b/lib/Quox/Equal.idr @@ -916,7 +916,8 @@ parameters (loc : Loc) (ctx : TyContext d n) (EqContext n -> DSubst d 0 -> Eff fs ()) -> Eff fs () eachCorner loc fvs act = do say "equal" 50 loc $ - hsep $ "eachCorner: split on" :: map prettyBind' (getVars ctx fvs) + let vars = map prettyBind' (getVars ctx fvs) in + hsep $ "eachCorner: split on" :: if null vars then ["(none)"] else vars for_ (splits loc ctx.dctx fvs) $ \th => act (makeEqContext ctx th) th