Tulip @hazel@types.pl

every day i wake up and i have to fucking reify

hello, website that i still run.

module nepeta where

open import Data.Nat
open import Relation.Binary.PropositionalEquality

data Buh {A : Set} (x : A) : Set where
  ꞉_<_ : (y : A) → (x ≡ y) → Buh x

what-are-you-talking-about : Buh 33
what-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

save your sanity

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

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

types.🇵🇱