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.
Scoped : Typethin : (0 ext : List Name) -> Check f g -> Check (ext ++ f) gthin : (0 ext : List Name) -> Infer f g -> Infer (ext ++ f) gclosed : (0 g : SnocList Name) -> Infer f [<] -> Infer f gthin : (0 ext : List Name) -> Value f -> Value (ext ++ f)