An encodable type is a "constructively countable" type. This is where we have an explicit injection encode : α → nat and a partial inverse decode : nat → option α. This makes the range of encode decidable, although it is not decidable if α is finite or not.