@@ -551,7 +551,7 @@ runLoop fuel prog onEmpty
551||| runWith allows running an STrans program with an initial environment,
551||| runWith allows running an STrans program with an initial environment,
552||| which must be consumed.
552||| which must be consumed.
553||| It's only allowed in the IO monad, because it's inherently unsafe, so
553||| It's only allowed in the IO monad, because it's inherently unsafe, so
554−||| we don't want to be able to use it under a 'lift in just *any* ST program -
554+||| we don't want to be able to use it under a 'lift' in just *any* ST program -
555||| if we have access to an 'Env' we can easily duplicate it - so it's the
555||| if we have access to an 'Env' we can easily duplicate it - so it's the
556||| responsibility of an implementation of an interface in IO which uses it
556||| responsibility of an implementation of an interface in IO which uses it
557||| to ensure that it isn't duplicated.
557||| to ensure that it isn't duplicated.
@@ -597,10 +597,12 @@ st_precondition (CantUnify _ tm1 tm2 _ _ _)
598 getPreconditions : TT -> Maybe TT
598 getPreconditions : TT -> Maybe TT
599 getPreconditions `(STrans ~m ~ret ~pre ~post) = Just pre
599 getPreconditions `(STrans ~m ~ret ~pre ~post) = Just pre
600+ getPreconditions `(STransLoop ~m ~ret ~pre ~post) = Just pre
600 getPreconditions _ = Nothing
601 getPreconditions _ = Nothing
602 getPostconditions : TT -> Maybe TT
603 getPostconditions : TT -> Maybe TT
603 getPostconditions `(STrans ~m ~ret ~pre ~post) = Just post
604 getPostconditions `(STrans ~m ~ret ~pre ~post) = Just post
605+ getPostconditions `(STransLoop ~m ~ret ~pre ~post) = Just post
604 getPostconditions _ = Nothing
606 getPostconditions _ = Nothing
606 renderPre : TT -> TT -> List (ErrorReportPart)
608 renderPre : TT -> TT -> List (ErrorReportPart)