anyone in the chat ever
(cons (value-Π 'A (value-Type) (closure (syntax-Π '_ (syntax-local 0) (syntax-local 1)) '())) (syntax-lam 'A (syntax-lam 'a (syntax-local 0))))
im very much looking forward to introducing dependent typechecking at this point
i think the way ive structured this entire course has led up to this moment and its ready for it to flourish :)
@hazel i don't know what any of this is, but i see lisp syntax and i am happy
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.
im very much looking forward to introducing dependent typechecking at this point
i think the way ive structured this entire course has led up to this moment and its ready for it to flourish :)