Countable types #
In this file we provide basic instances of the Countable
typeclass defined elsewhere.
Definition in terms of Function.Embedding
#
Operations on Type _
s #
Equations
instance
instCountableSigma
{α : Type u}
{π : α → Type w}
[inst : Countable α]
[inst : ∀ (a : α), Countable (π a)]
:
Operations on Sort _
s #
Equations
instance
instCountablePSigma
{α : Sort u}
{π : α → Sort w}
[inst : Countable α]
[inst : ∀ (a : α), Countable (π a)]
: