3.1. Das Provas aos Programas🔗

A Aula 1 apresentou uma prova como um termo cujo tipo é a proposição que ela prova. A mesma teoria de tipos classifica dados. Um tipo como ℕ reúne valores, e um termo de tipo ℕ → ℕ é um programa que consome e produz valores. O #check abaixo se lê exatamente como o #check de um termo de prova, com tipos no lugar de proposições.W. A. Howard, The Formulae-as-Types Notion of Construction, em To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, 1980, pp. 479–490.

fun n => n + 1 : ℕ → ℕ

Esta aula define tipos e funções e enuncia teoremas sobre eles. As provas desses teoremas esperam pelas próximas aulas, que desenvolvem a indução estrutural. Esta aula também importa a biblioteca LoVe e, por meio dela, Mathlib, a biblioteca matemática da comunidade Lean.The mathlib Community, The Lean Mathematical Library, em Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. Mathlib é um desenvolvimento monolítico único que formaliza álgebra, teoria da ordem, topologia, análise e as estruturas de dados usuais, e fornece as notações, os lemas e as táticas de que o restante destas aulas depende. As notações ℕ e ℤ para os números naturais e os inteiros vêm dela e são usadas daqui em diante.