The math book rewritten with implicit arguments

I have rewritten my math book (volume 1) with implicit arguments (that is I sometimes write \bot instead of \bot^{\mathfrak{A}} to denote the least element of the lattice \mathfrak{A}).

It considerably simplifies the formulas.

If you want to be on this topic, learn what is called “dependent lambda calculus”. (Sadly, I do not use it in my book explicitly, in order to make my book easier to understand. But I weight the possibility to rewrite my book in a dependent lambda calculus proof-assistant language, that is in the language of an automatic proof verification software, to make it even greater.)

Leave a Reply