Additional theorems and definitions about the Vector
type #
This file introduces the infix notation ::ᵥ
for Vector.cons
.
If a : α
and l : Vector α n
, then cons a l
, is the vector of length n + 1
whose first element is a and with l as the rest of the list.
Equations
Instances For
The empty Vector
is a Subsingleton
.
The recursive step of scanl
splits a vector x ::ᵥ v : Vector α (n + 1)
into the provided starting value b : β
and the recursed scanl
f b x : β
as the starting value.
This lemma is the cons
version of scanl_get
.
The toList
of a Vector
after a scanl
is the List.scanl
of the toList
of the original Vector
.
The recursive step of scanl
splits a vector made up of a single element
x ::ᵥ nil : Vector α 1
into a Vector
of the provided starting value b : β
and the mapped f b x : β
as the last value.
For an index i : Fin n
, the nth element of scanl
of a
vector v : Vector α n
at i.succ
, is equal to the application
function f : β → α → β
of the castSucc i
element of
scanl f b v
and get v i
.
This lemma is the get
version of scanl_cons
.
Define C v
by induction on v : Vector α n
.
This function has two arguments: nil
handles the base case on C nil
,
and cons
defines the inductive step using ∀ x : α, C w → C (x ::ᵥ w)
.
It is used as the default induction principle for the induction
tactic.
Equations
Instances For
Define C v w
by induction on a pair of vectors v : Vector α n
and w : Vector β n
.
Equations
Instances For
Define C u v w
by induction on a triplet of vectors
u : Vector α n
, v : Vector β n
, and w : Vector γ b
.
Equations
Instances For
Define motive v₁ v₂
by case-analysis on v₁ : Vector α n
and v₂ : Vector β n
.
Equations
Instances For
Define motive v₁ v₂ v₃
by case-analysis on v₁ : Vector α n
, v₂ : Vector β n
, and
v₃ : Vector γ n
.
Equations
Instances For
Apply an applicative function to each component of a vector.