Commit 36363712 authored by Ralf Jung's avatar Ralf Jung
parents 1de37fd6 e1d492b8
Pipeline #4068 passed with stage
in 1 minute and 59 seconds
......@@ -359,12 +359,12 @@ Qed.
Lemma vlookup_insert_self {A n} i (v : vec A n) : vinsert i (v !!! i) v = v.
Proof. by induction v; inv_fin i; intros; f_equal/=. Qed.
(* Vectors can be inhabited. *)
Global Instance vec_nil_inh T : Inhabited (vec T 0) := populate [#].
(** The function [vreplicate n x] generates a vector with length [n] of elements
with value [x]. *)
Fixpoint vreplicate {A} (n : nat) (x : A) : vec A n :=
match n with 0 => [#] | S n => x ::: vreplicate n x end.
Global Instance vec_inh T n : Inhabited T Inhabited (vec T n).
Proof.
intros HT. induction n; [apply _|].
destruct IHn as [v]. destruct HT as [x].
exact (populate (x:::v)).
Qed.
(* Vectors can be inhabited. *)
Global Instance vec_0_inhabited T : Inhabited (vec T 0) := populate [#].
Global Instance vec_inhabited `{Inhabited T} n : Inhabited (vec T n) :=
populate (vreplicate n inhabitant).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment