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.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
