@@ -122,10 +122,11 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _ _) =
122 prettyPs bnd ((n@(MN _ r), _) : bs)
122 prettyPs bnd ((n@(MN _ r), _) : bs)
123 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
123 | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
124 prettyPs bnd ((n, Let t v) : bs) =
124 prettyPs bnd ((n, Let t v) : bs) =
125− nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
125+ line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>
126− tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
126+ align (tPretty bnd t) <> prettyPs ((n, False):bnd) bs
127 prettyPs bnd ((n, b) : bs) =
127 prettyPs bnd ((n, b) : bs) =
128+ line <> bindingOf n False <+> colon <+>
128− line <> bindingOf n False <+> colon <+> align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
129+ align (tPretty bnd (binderTy b)) <> prettyPs ((n, False):bnd) bs
130 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
131 prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
131 prettyG bnd b = tPretty bnd $ binderTy b
132 prettyG bnd b = tPretty bnd $ binderTy b