Programming in Lean

• 1. Introduction
• 2. Types and Terms
  • 2.1. Some Basic Types
  • 2.2. Defining Functions
  • 2.3. Defining New Types
  • 2.4. Records and Structures
  • 2.5. Mathematics and Computation
• 3. Basic Programming
  • 3.1. Evaluating Expressions
  • 3.2. Recursive Definitions
  • 3.3. Inhabited Types, Subtypes, and Option Types
  • 3.4. Input and Output
• 4. Monads
  • 4.1. The option monad
  • 4.2. The list monad
  • 4.3. The state monad
  • 4.4. The IO monad
  • 4.5. Related type classes
• 5. Writing Tactics
  • 5.1. A First Look at the Tactic Monad
  • 5.2. Names and Expressions
  • 5.3. Examples
  • 5.4. Reduction
  • 5.5. Metavariables and Unification
• 6. Writing Automation
  • 6.1. A Tableau Prover for Classical Propositional Logic