File tree 1 file changed +2
-2
lines changed
1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -71,12 +71,12 @@ Arguments vnil {_}.
71
71
Arguments vcons {_} _ _ _.
72
72
73
73
(** The difference between a parameter and an index is that a parameter is
74
- constant accros all the return types of the constructors, whereas an index
74
+ constant accross all the return types of the constructors, whereas an index
75
75
changes in at least one of the return types.
76
76
For instance, in the definition of vectors the type [A] is a parameter
77
77
as it is constant across all the return types: [vec A 0] and [vec A (S n)].
78
78
However, [n:nat] is an index as it is not constant in the returns types:
79
- in the return type of [vnil] it is fixed to [0], and in the return type of [vcons] it is [S n].
79
+ in the return type of [vnil] it is fixed to [0], and in the return type of [vcons] it is [S n].
80
80
Indices always appear after the [:] in an inductive type declaration.
81
81
82
82
Reasoning about indexed inductive types like vectors is a bit more
You can’t perform that action at this time.
0 commit comments