NF-exp₂ : NF exp₂
NF-exp₂ (.(Lam "z" _) , ζ (BETA⟶ ()))

statements made by the utterly deranged

@amy i shrimply press C-c C-c until it goes 👍

@amy oh also this file uses --sized-types. awful

Sign in to participate in the conversation
types.pl

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.