From 311fed09e8fb0fcd687c774862cbefd4faa5efe3 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Mon, 28 Oct 2024 17:08:50 +0000 Subject: [PATCH] Use ReaderT.local instead of |>.local for clarity --- lean/Raylean/Graphics2D/Render.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lean/Raylean/Graphics2D/Render.lean b/lean/Raylean/Graphics2D/Render.lean index 57997f3..6c72fcc 100644 --- a/lean/Raylean/Graphics2D/Render.lean +++ b/lean/Raylean/Graphics2D/Render.lean @@ -49,11 +49,11 @@ partial def renderPicture' : (picture : Picture) → ReaderT RenderContext IO Un | .line ps => renderLine ps | .circle radius => renderCircle radius | .rectangle width height => renderRectangle width height - | .color c p => renderPicture' p |>.local (set color c) - | .translate v p => renderPicture' p |>.local (fun s => + | .color c p => ReaderT.local (set color c) (renderPicture' p) + | .translate v p => ReaderT.local (fun s => over translate (·.add (v.dot s.scale)) s - ) - | .scale v p => renderPicture' p |>.local (over scale (·.dot v)) + ) (renderPicture' p) + | .scale v p => ReaderT.local (over scale (·.dot v)) (renderPicture' p) | .pictures ps => (fun _ => ()) <$> ps.mapM renderPicture' def renderPicture (width height : Float) (picture : Picture) : IO Unit :=