## Library Vecs

## Library Vecs.Util

## Library Vecs.VecBase

- Lists indexed by their length.
- The Vec type.
- Primitive functions.
- The proposition that a list contains some element.
- The proposition that all elements of one list are contained in another.

## Library Vecs.VecEq

- Propositional and boolean John-Major equality for Vec.
- John Major propositional equality for Vec.
- Boolean equality for Vec.

## Library Vecs.VecMap

## Library Vecs.VecFilter

## Library Vecs.VecAppend

## Library Vecs.VecReverse

- Reversing functions and induction principles
- Facts about rev
- Reverse induction principle on Vec
- Left-recursive induction principle on Vec

## Library Vecs.VecInduction

## Library Vecs.VecFold

## Library Vecs.VecAlgebra

## Library Vecs.VecMonad

## Library Vecs.VecTake

## Library Vecs.VecLookup

This page has been generated by coqdoc