Finiteness of FunLike
types #
We show a type F
with a FunLike F α β
is finite if both α
and β
are finite.
This corresponds to the following two pairs of declarations:
FunLike.fintype
is a definition stating allFunLike
s are finite if their domain and codomain are.FunLike.finite
is a lemma stating allFunLike
s are finite if their domain and codomain are.FunLike.fintype'
is a non-dependent version ofFunLike.fintype
andFunLike.finite
is a non-dependent version ofFunLike.finite
, because dependent instances are harder to infer.
You can use these to produce instances for specific FunLike
types.
(Although there might be options for Fintype
instances with better definitional behaviour.)
They can't be instances themselves since they can cause loops.
All FunLike
s are finite if their domain and codomain are.
This is not an instance because specific FunLike
types might have a better-suited definition.
See also FunLike.finite
.
Instances For
All FunLike
s are finite if their domain and codomain are.
Non-dependent version of FunLike.fintype
that might be easier to infer.
This is not an instance because specific FunLike
types might have a better-suited definition.
Instances For
All FunLike
s are finite if their domain and codomain are.
Non-dependent version of FunLike.finite
that might be easier to infer.
Can't be an instance because it can cause infinite loops.