Language.TypeTheory

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: The work is originally written in Haskell and uses unsafe features
    This is not how we would write idiomatic Idris code.
    Cf. Language.IntrinsicScoping.TypeTheory for a more idiomatic representation.

Definitions

data Name : Type

  Named variables

Totality: total
Visibility: public export
Constructors:

Global : String -> Name

  The most typical of name: external functions

Local : Nat -> Name

  When passing under a binder we convert a bound variable
  into a `Local` free variable

Quote : Nat -> Name

  During quoting from values back to term we will be using
  the `Quote` constructor

Hint: 

Eq Name

fromInteger : Integer -> Infer

Visibility: public export

fromString : String -> Check

Visibility: public export

fromInteger : Integer -> Check

Visibility: public export

fromString : String -> Ty

Visibility: public export