makarius at sketis.net
Thu Sep 10 17:06:50 CEST 2015
On Thu, 10 Sep 2015, Larry Paulson wrote:
> Purely FYI: the names of all of these constants were originally based on
> the corresponding names in Martin-Löf type theory.
I do remember the good old times of MLTT, where it was clear what the
basic combinators are.
Interestingly, MLTT is up-to-date once again, in the guise of HoTT. I now
wonder if these guys have a 15th standard of naming things, or are using
the primordial one.
More information about the isabelle-dev