Package telescope - Namespaces

• Data.Telescope

  A telescope is the variable context in a dependently typed program. Dependent types with free variables are really only well-defined in a telescope.
• Data.Telescope.Congruence

  N-ary congruence for reasoning
• Data.Telescope.Fun

  N-ary dependent functions using telescopes
• Data.Telescope.Segment

  A segment is a compositional fragment of a telescope. A key difference is that segments are right-nested, whereas telescopes are left nested. So telescopes are convenient for well-bracketing dependencies, but segments are convenient for processing telescopes from left to right.
• Data.Telescope.SimpleFun

  N-ary simple (non-dependent) functions using telescopes
• Data.Telescope.Telescope

  The telescope data structures.