This repository contains the Agda code associated with the paper "D. Firsov, T. Uustalu. Dependently Typed Programming with Finite Sets" published at WGP 2015.
- Finiteness.agda -Listable sets and listable subsets.
- Examples/Pauli.agda - The example of a straightforward approach of defining new finite.
- Combinators.agda - Basic combinators on listable sets and subsets.
- Examples/Combinators.agda - Simple example of using combinators.
- FiniteSubset.agda - The alternative way of defining the new finite sets as a subsets.
- Tabulation.agda - Defining new functions from finite sets by providing an explicit; table + proofs of correctness.
- Examples/Tabulation.agda - Example of a function definition by using tables.
- PredicateMatching.agda - Defining new functions from the list of predicate--function pairs and proofs of correctness.
- Prover.agda - Prover for propositions quantified over finite sets.
- Examples/Prover.agda - Comapring the approaches of automatically deriving the properties for finite types.
Agda @ 2.6.0.1, agda-stdlib @ 1.1-1