Show newer

the year is 2023 please give me a positive definition for normal forms i will cry

Show thread

me when someone defines a normal form as a term with no beta redexes and expects me to do anything with that information

..i may have horrible executive dysfunction

Show thread

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 :verified_dragon: boosted

every day i wake up and i have to fucking reify

such wonderful options as:
- semidecidable
- serious
- silly
- sex
- scheme
- soviet
- serket
- shhhh

Show thread

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


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

Show thread

wow i should probably update this website. oh huh what's that

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 :)

Show thread

anyone in the chat ever

(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

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

Show older

Tulip :verified_dragon:'s choices:

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