Abstract
Definitions of many mathematical structures used in computer science are parametrized by finite sets. To work with such structures in proof assistants we need to be able to explain when a set is finite. In constructive mathematics, a widely used definition is finite enumerability: a set is considered finite if it can be completely listed. In this paper, we formalize different variations of this definition in the Agda programming language. We develop a toolbox for boilerplate-free programming with finite sets that arise as subsets of some base set with decidable equality. Among other things we implement combinators for defining functions from finite sets and a prover for quantified formulas over decidable properties on finite sets.