2022 Developer Survey is open! Take survey.

Questions tagged [hol-light]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
4 votes
2 answers

What is the relation of HOL Light type theory and some of the intuitionistic type theories?

I'm trying to understand how HOL Light deductive rules relate to mainstream intuitionistic type theories. Here is a sample of questions that come to my mind. Does ...
user avatar
  • 1,147
3 votes
1 answer

Why REFL rule is primitive in HOL Light?

HOL Light assumed REFL as a primitive. Why does it need to do so? Can't REFL rule be deduced in this way using ...
user avatar
  • 1,147