if you first press the ' key and then the e key, the resulting é depends on both keys. this is called "dependent typing"

· · Web · 2 · 2 · 1

half true facts. half misinfo 

polish switched away from having special keys to using a modifier key. this started after Martin-Löf's 1980 München lecture series, for which he adapted dependent type theory to Polish notation.


@Vierkantor dependently typed language (french)

Sign in to participate in the conversation

Mastodon is a server for a federated social network: everyone can run a server if they want to, including me. So this is a Mastodon server for me (Vierkantor) and my friends.