I think it would be interesting to do a metastudy on metasyntax and how people write things, especially in dependent type theory
I know someone already did one for all the different notations people use for substitution but there's a lot more than just that
I don't know what questions would be interesting to ask though

re: dependent pairs

I'm adding pairs and I was wondering about this again. I'm glad I wondered about this in the past so I don't have to do it again, but I realize I never really actually stepped through whatever inconsistency proof it was with dependent pairs in prop

I gotta say, though, defining a lot of small rules is a lot more digestible than defining one gigantic frankenrule for case expressions

It's annoying that for every new construct I add to my language, I need to add the type former, the introduction form, the elimination form, and typing rules for all of these
If only there were some generalized way of defining all of these once and for all

​ help

@hazel
when the imposter (proof term) is sus (refl)

LaTeX

This macro

\WithSuffix\newcommand\Pair*[2]{#1 \mathbin{\times} #3}

gives this rather obtuse error

Illegal parameter number in definition of \WSF:\Pair the character *.

but you know what? It's right. I just can't read. I used #3 instead of #2
That took a bit to debug

To quote @vdash,

There is so much about equality. I feel like 99% of type theory is about equality

Why does Elasticsearch keep stopping!! What's going on

Can you believe I spent a month trying to find a semantically-justified representation of the infinite size only for a simple isInfinite? function to hold more promise than HITs or quotient types ever did

Equational reasoning who? All I know is rewrite

Agda code

I got nerd sniped and this is what happened

Looks like it's because I'm employed as a TA

Apparently I can apply for a staff card at my university because I'm an employee and I have an employee number

They're now all divided up into tidy little (too many) folders
idk what the point is but I've done it

I spent the morning organizing my emails

Once I had to say the word "redexes" out loud for whatever reason and I had to stop myself from saying "redices"

If I spent as much time figuring out what I need to install as I did complaining would I have it working by now? Probably not. Guess I should spend some more time complaining to balance it out

(It's not my tablet but I'm the only one using it so it might as well be mine now)

One of these days I'll properly figure out how to get my tablet to work on Manjaro

Show older

A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.