Welcome to coproducts-lean, a Lean 4 library designed to enhance functional programming in Lean with coproduct types. Our library offers a robust set of tools for handling multiple types of return values, error handling, and data alignment in a functional programming context. By leveraging coproducts like Validation, These, and Attempt, developers can write more expressive and flexible code.
- Validation Type: A type representing either a success with a value or a failure with an error, capable of accumulating errors.
- These Type: A versatile type indicating either a value, an error, or both, facilitating operations on partial data.
- Attempt Type: Similar to
Validationbut includes apartialSuccessstate for nuanced error and success handling. - Functor, Applicative, and Monad Instances: Comprehensive instances for these types, enabling powerful functional programming patterns.
- Semialign and Align Type Classes: For aligning data structures, supporting operations with potentially missing elements.