Idris2Doc : Language.IntrinsicScoping.TypeTheory

Language.IntrinsicScoping.TypeTheory(source)

The content of this module is based on the paper:
A tutorial implementation of a dependently typed lambda calculus
by Andres Löh, Conor McBride, and Wouter Swierstra

NB: Unlike `Language.TypeTheory`, this is not a direct translation
    of the code in the paper but rather a more idiomatic solution.

Definitions

Scoped : Type: Visibility: public export
thin : (0 ext : List Name) -> Check f g -> Check (ext ++ f) g: Visibility: export
thin : (0 ext : List Name) -> Infer f g -> Infer (ext ++ f) g: Visibility: export
closed : (0 g : SnocList Name) -> Infer f [<] -> Infer f g: Visibility: export
thin : (0 ext : List Name) -> Value f -> Value (ext ++ f): Visibility: export