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

· · Web · 0 · 0 · 1
Sign in to participate in the conversation

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