Library Vecs

• Lists indexed by their length.

Library Vecs.Util

• Assorted utility functions we can't find anywhere else.
  • Arithmetic on nat
  • The option type

Library Vecs.VecBase

• Lists indexed by their length.
• The Vec type.
• Primitive functions.
  • Peeking and popping from the ends of a list.
  • Facts about injectivity and surjectivity.
  • Facts about cons.
  • Other facts which aren't specifically cons or snoc focused.
  • Facts about snoc.
• The proposition that a list contains some element.
  • Facts about In
• The proposition that all elements of one list are contained in another.
  • Smart constructors for Vec

Library Vecs.VecEq

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

Library Vecs.VecMap

• Mapping functions for lists indexed by their length.
• Vec is a functor.
  • Facts about map.

Library Vecs.VecFilter

• Filtering a list with a predicate

Library Vecs.VecAppend

• Appending lists indexed by their length.

Library Vecs.VecReverse

• Reversing functions and induction principles
• Facts about rev
  • Compatibility with other operations
• Reverse induction principle on Vec
• Left-recursive induction principle on Vec

Library Vecs.VecInduction

• Additional induction principles for lists indexed by their length.

Library Vecs.VecFold

• Folding operations for lists indexed by their length.

Library Vecs.VecAlgebra

• Algebraic reasoning for lists indexed by their length.
• Explicit algebras and coalgebras

Library Vecs.VecMonad

• Monadic interface for lists indexed by their length.
• Vec is a monad
  • Facts about concatMap.

Library Vecs.VecTake

• Getting prefixes and suffixes of lists indexed by their length.

Library Vecs.VecLookup

• Lookup functions for lists indexed by their length.

---

This page has been generated by coqdoc