Lean code for an agent in a Cartesian environment CartesianAgent.lean contains general definitions. RotationWorld.lean contains code describing a grid world with rotation and implements part of the interface described in CartesianAgent.lean.