Lean Portfolio

This page gives an overview of some of my Lean projects.

lean-ios

A framework for building and running Lean applications on iOS simulators and devices.

It includes:

1. A modified lean4 source repository that’s compatible with the iOS toolchain
2. Build scripts for the Lean runtime, stdlib, and Lean programs for iOS
3. Lean SDL3 FFI bindings
4. Example applications, including a Flappy Bird game

lean-effects

A scoped algebraic effects library for Lean. The implementation is based on an Agda library by Jonas Höfer. One of the main challenges in the implementation was how to define the Prog type. In order for Lean to accept the doubly-nested inductive type (needed to define scoped effect handlers), a nested induction is required.

lens-demo

A demo lens library for Lean. Lenses are composable functional references for immutable data access and update.

It uses metaprogramming to generate the lens definition boilerplate for a structure automatically.

lean-ecs

An entity component system (ECS) library for Lean. ECS is a common architectural pattern in game development.

Users can write functions over particular combinations of components and these are translated to entity updates via instance resolution.

It uses metaprogramming to generate the boilerplate needed to set up the ECS for user-specified components.

raylean

Lean bindings for the raylib library for graphics and game programming.

orbital

An orbital mechanics simulator built using raylean and lean-ecs.

flappy

A Flappy Bird game written built using raylean.

lean-pan

An experiment in using SIMD to accelerate CPU framebuffer rendering in Lean.