Skip to content

Commit

Permalink
Merge pull request #44 from paulcadman/improve-global-entity
Browse files Browse the repository at this point in the history
Improve API for global entity
  • Loading branch information
paulcadman authored Nov 9, 2024
2 parents f445c75 + 311fed0 commit 10b75bf
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions lean/Raylean/Graphics2D/Render.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down

0 comments on commit 10b75bf

Please sign in to comment.