-Fixpoint list2vecOrError {T}(l:list T)(n:nat) : ???(vec T n) :=
- match n as N return ???(vec _ N) with
- | O => match l with
- | nil => OK vec_nil
- | _ => Error "list2vecOrError: list was too long"
- end
- | S n' => match l with
- | nil => Error "list2vecOrError: list was too short"
- | t::l' => list2vecOrError l' n' >>= fun l'' => OK (vec_cons t l'')
- end
- end.
-