You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
I explained in three blog posts (parts one, two, three) how to implement a small dependent type theory. The language tt is suitable for the PL zoo (and in fact, I stole code from the old PL zoo to implement tt). The repo for tt is at https://github.com/andrejbauer/andromeda (branches blog-part-I, blog-part-II and blog-part-III). Probably the part-III version is most suitable for the PL Zoo.
The text was updated successfully, but these errors were encountered:
I explained in three blog posts (parts one, two, three) how to implement a small dependent type theory. The language
tt
is suitable for the PL zoo (and in fact, I stole code from the old PL zoo to implementtt
). The repo fortt
is at https://github.com/andrejbauer/andromeda (branchesblog-part-I
,blog-part-II
andblog-part-III
). Probably the part-III version is most suitable for the PL Zoo.The text was updated successfully, but these errors were encountered: