Tulip 
@hazel@types.pl
Admin
types.pl admin. they.
math & computer science student at indiana university bloomington. it's been conjectured that i exist but nobody's been able to prove it.
this is decidedly my shop talk account. if you know me relatively well, feel free to ask me for my non-work posts.
Joined Oct 2020
type theory
the year is 2023 please give me a positive definition for normal forms i will cry
me when someone defines a normal form as a term with no beta redexes and expects me to do anything with that information
what the fuck is a cube
i should probably apply to that pl reu huh
NF-exp₂ : NF exp₂
NF-exp₂ (.(Lam "z" _) , ζ (BETA⟶ ()))
statements made by the utterly deranged
Tulip
boosted
boosted
every day i wake up and i have to fucking reify
such wonderful options as:
- semidecidable
- serious
- silly
- sex
- scheme
- soviet
- serket
- shhhh
less bit-y way of announcing it
i'm changing my name from Hazel Levine to Tulip S. Amalie, effective immediately
the S stands for whatever i feel like at the time
Q&A:
why? oh you know
what's the s stand for? oh you know
why the last name amalie? oh you know
are you going to get this changed legally? wow that's invasive. but probably
oh i know oh you know
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 :)
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))))
the time has come in the class i'm teaching about type theory where i go "so we're doing dependent types now. everything i have told you is either a lie or a massive oversimplification."
every day i wake up and i have to fucking reify
hello, website that i still run.
extremely normal agda code
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
Admin
types.pl admin. they.
math & computer science student at indiana university bloomington. it's been conjectured that i exist but nobody's been able to prove it.
this is decidedly my shop talk account. if you know me relatively well, feel free to ask me for my non-work posts.
Joined Oct 2020
Tulip 's choices:
