🐔
Let's play Agda Beta

Welcome
Agda as a programming language
Agda as a proof language
1. Predicates on natural numbers
2. Negation
3. Equality
4. Logical connectives
5. Termination and well-founded recursion
Verified algorithms
1. Post-hoc verification
2. Correct by construction
3. Case study: Insertion sort
  1. Implementation
  2. Post-hoc verification
4. Case study: Compiler and interpreter
Cubical Agda
1. Issues with standard Agda
  1. Function extensionality
  2. Quotients
  3. The identity types of the universe
2. A mathematical rosetta stone
3. First steps
Computational content of classical logic
1. Convenient fictions
  1. Minimas
  2. Drinkers
2. Sarcastic interpretation of classical logic
3. Case study: Dickson's lemma

📥 Download raw

module Padova2025.ProgrammingBasics.Naturals where

Natural numbers

In the previous chapter, we have defined the finite type of Booleans. Agda also supports infinite types. The natural numbers are the primordial example, and we will explore them now.

import Padova2025.ProgrammingBasics.Naturals.Base
import Padova2025.ProgrammingBasics.Naturals.Arithmetic
import Padova2025.ProgrammingBasics.Naturals.DecisionProcedures