Eliminators are undoubtedly the most difficult aspect of type theory. In this article we will try to make more clear how they work, but most importantly why we need them. This article will present some analogies between eliminators and constructs of programming languages (such Python, Rust, Scala, …) which can help who knows some basic of computer programming understanding eliminators.
I'm Italian and I don't like pasta al dente. Obviously neither overcooked, but I like it cooked. In fact it's a drama that since some years they started making pasta which remains al dente: I usually cook it at least 5 minutes longer than what is written and it is still slightly al dente: very disappointing.
You can increase the guess accuracy a little by looking for the "tLS" characters , skipping the first 3 chars. Also this is a mnemonic about TLS and identifies all strings starting with 5 dashes, excluding so most of yaml documents
Theoretically only one operation is sufficient: both NAND and NOR are universal gates, meaning all boolean operations are expressible in terms of only NANDs (or equivalently only NORs). The downside is that the expressions became longer.
Web version: https://dpdmancul.gitlab.io/blog/2023/01/eliminators