Toy typechecker for Insanely Dependent Types
Haskell
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Failed to load latest commit information.
typechecker
.gitignore
Context.agda
Makefile
README
Sigma.agda

README

Toy implementation of Insanely Dependent Types

Features

  - Insane pi-types:

      [x1 : A1, x2 : A2, .., xn : An] -> B

    All xi are in scope in the Ai's (and in B of course). Applications of
    insane functions must be fully applied.

  - Everything is mutually recursive

  - Simple Agda-like syntax

Limitations

  - No implicit arguments
  - Function types and Set are not terms
  - No indexed datatypes