Skip to main content

Questions tagged [hol]

Use this tag for the HOL Interactive Theorem Prover. Do not use this tag for other proof assistants in the HOL family such as HOL Light. For questions about higher order logic use the tag (higher-order-logic).

Filter by
Sorted by
Tagged with
18 votes
1 answer

How can all functions be total in Isabelle?

Isabelle/HOL’s logic is called a logic of “total functions”, yet there are functions that are obviously not total, such as division div. How does this make sense?
Joachim Breitner's user avatar
5 votes
1 answer

How can I derive other type classes in Isabelle/HOL?

The AFP entry Deriving provides a way to derive the following classes: class description comparator generate comparators for given types compare register types in class compare compare_order ...
Wno-all's user avatar
  • 1,118
5 votes
0 answers

Proof-theoretic strength of HOL compared to predicative dependent types

By HOL I mean something like inference rules of HOL Light with the 3 axioms of infinity, extensionality and choice ($\varepsilon$ operator). By predicative dependent types, I am thinking of MLTT + W-...
Ilk's user avatar
  • 547
0 votes
1 answer

How to reason with notations directly?

Intuitive notations are always a big boost when stating and proving things. Modern interactive theorem provers usually have some way of building syntactic sugars aside from their ordinary abstraction ...
yiyuan-cao's user avatar