Index lens.

>>> view (ix (FS FZ)) ('a' ::: 'b' ::: 'c' ::: VNil)
'b'

>>> set (ix (FS FZ)) 'x' ('a' ::: 'b' ::: 'c' ::: VNil)
'a' ::: 'x' ::: 'c' ::: VNil

Match on non-empty Vec.

Note: lens _Cons is a Prism. In fact, Vec n a cannot have an instance of Cons as types don't match.

Head lens. Note: lens _head is a Traversal'.

>>> view _head ('a' ::: 'b' ::: 'c' ::: VNil)
'a'

>>> set _head 'x' ('a' ::: 'b' ::: 'c' ::: VNil)
'x' ::: 'b' ::: 'c' ::: VNil

Tail lens.

An Iso from toPull and fromPull.

Prism from list.

>>> preview _Vec "foo" :: Maybe (Vec N.Nat3 Char)
Just ('f' ::: 'o' ::: 'o' ::: VNil)

>>> preview _Vec "foo" :: Maybe (Vec N.Nat2 Char)
Nothing

>>> review _Vec (True ::: False ::: VNil)
[True,False]