Documentation

Apply a context to a term (i.e., replace the hole in the context by the term).

Compose two contexts (i.e., replace the hole in the left context by the right context).

Create a context from a term by placing the hole at a specific position.