当您看到一个类型族时，您可能想知道它的每个参数是否都是参数 or indices.
参数仅表明该类型有些通用，并且行为参数化地关于所提供的论点。
例如，这意味着类型List T无论哪个都会具有相同的形状T你考虑：nil, cons t0 nil, cons t1 (cons t2 nil)等的选择T只影响可以插入的值t0, t1, t2.
Indices另一方面可能会影响您可以在该类型中找到哪些居民！这就是为什么我们说他们index类型族，即每个索引告诉您正在查看的类型（类型族内）中的哪一个（从这个意义上说，参数是一种退化情况，其中所有索引都指向同一组“形状”）。
例如，类型族Fin n或大小有限集n根据您的选择包含非常不同的结构n.
指数0索引一个空集。
指数1用一个元素索引一组。
从这个意义上说，对指数价值的了解可能携带着重要的信息！通常，您可以通过查看索引来了解哪些构造函数可能已使用或未使用。这就是依赖类型语言中的模式匹配如何消除不可行的模式，并从模式的触发中提取信息的方式。
这就是为什么当你定义归纳族时，通常你可以定义整个类型的参数，但你必须为每个构造函数指定索引（因为你可以为每个构造函数指定它所在的索引）。
例如我可以定义：
F (T : Type) : ℕ → Type
C1 : F T 0
C2 : F T 1
C3 : F T 0
Here, T是一个参数，而0 and 1是指数。当你收到一些x类型的F T n，看什么T不会透露任何有关x。但看着n会告诉你：
- that
x必须是C1 or C3 when n is 0
- that
x必须是C2 when n is 1
- that
x否则一定是从矛盾中伪造出来的
同样，如果您收到y类型的F T 0，你知道你只需要模式匹配C1 and C3.
