every day i wake up and i have to fucking reify

hello, website that i still run.

extremely normal agda code

module nepeta whereopen import Data.Natopen import Relation.Binary.PropositionalEqualitydata Buh {A : Set} (x : A) : Set where  ꞉_<_ : (y : A) → (x ≡ y) → Buh xwhat-are-you-talking-about : Buh 33what-are-you-talking-about = ꞉ 33 < refl

all new agda burger which you order via the webapp but you just get the wrapper and in order to get the actual burger you have to follow a seven step process that involves editing a text file

"what's equality" - the greatest thread in the history of programming languages, locked after 8130 pages of debate,

meow

Hazel

I am not doing Advent of Code and I would recommend also not doing Advent of Code

WHO THE FUCK IS SCREAMING "REIFY" AT MY WINDOW. SHOW YOURSELF COWARD. I WILL NEVER REIFY.

type theory (DEROGATORY)

She mon-in on my ad 'til I attempt to get a trace of linear execution and fuck up the entire stack.

just realized that none of these words are real

bogos bingus

bingus binthesized 👽

bingus

Tulip boosted

ICYMI: Hazel Levine (Indiana) at

Design Recipe Guided Synthesis with Bingus

youtu.be/oAE_G6HYilo

Source for Bingus github.com/ralsei/bingus

​​ ← what is this country and why are all the girls from here into type theory

types.🇵🇱

Show older

Tulip 's choices:

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