flatten package:Agda

An interpreter for OccurrencesBuilder. WARNING: There can be lots of sharing between the generated OccursWhere entries. Traversing all of these entries could be expensive. (See computeEdges for an example.)

Compute a flattened scope. Only include unqualified names or names qualified by modules in the first argument.

Turn a context into a flat telescope: all entries live in the whole context. (Γ : Context) -> [Type Γ]

Flatten telescope: (Γ : Tel) -> [Type Γ]

Unflatten: turns a flattened telescope into a proper telescope. Must be properly ordered.

A variant of unflattenTel which takes the size of the last argument as an argument.