rachel/pi
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
A typechecker for intensional MLTT without elaboration.
15 Commits 1 Branch 0 Tags 912 KiB
Idris 99.4%
Makefile 0.6%
752b6ee4c9
Go to file
depsterr 752b6ee4c9 updated TODO priorities
2022-07-21 04:26:06 +02:00
src added Σ types 2022-07-21 04:18:50 +02:00
.gitignore initial commit 2022-04-23 15:18:06 +02:00
makefile initial commit 2022-04-23 15:18:06 +02:00
pi.ipkg it works ! a lot has changed 2022-05-13 19:46:05 +02:00
README.md updated TODO priorities 2022-07-21 04:26:06 +02:00

README.md

pi

A dependently typed system

Implemented

  • A Basic dependent lambda calculus

    • lambda abstractions
    • variables
    • pi types
    • type of types

  • Unit type

  • Empty type

  • Natural numbers

  • Σ Types

TODO

  • Let … in …

  • Parser

  • Fun types

    • Id

  • Universes

  • Implicit arguments

  • (indexed) inductive datatypes

  • Write down the rules (I’ll not get this far)

References

Some of the material I found helpful in groking dependent type checking: