GitHub - Mathnerd314/insane: Toy typechecker for Insanely Dependent Types

Mathnerd314 / insane Public

forked from UlfNorell/insane

Notifications You must be signed in to change notification settings
Fork 0
Star 1

Toy typechecker for Insanely Dependent Types

Notifications

Name		Name	Last commit message	Last commit date
Latest commit History 9 Commits
typechecker		typechecker
.gitignore		.gitignore
Context.agda		Context.agda
Makefile		Makefile
README		README
Setup.hs		Setup.hs
Sigma.agda		Sigma.agda
insane.cabal		insane.cabal

Repository files navigation

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