Lait
Lait is a simple programming language embedded in the Lean proof assistant, intended to be used for teaching programming languages courses. To get started using Lait, see here. If you are interested in the implementation of Lait itself, see the repository.
The Lait tutorial is meant to be read in order, from beginning to end:
- Getting Started
- Arithmetic and Basic Commands
- Boolean Operators
- Strings
- Product Types
- Creating Simple Definitions:
letanddef - Functions
- Polymorphism
- Complex Data, Part I: Lists and Option
- Complex Data, Part II: User-Defined Types
- Type Aliases
- Printing and the Unit type
- Mutable References
- Errors
Additional information about functions and datatypes built in with Lait are here.