Skip to main content
17 votes
Accepted

How can all functions be total in Isabelle?

If you have a Isabelle/HOL function f :: a ⇒ b between two types a and b (NB: the function ...
Joachim Breitner's user avatar
3 votes

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

To register a new type class with the Deriving_Manager, I found Derive_Aux.define_overloaded useful. Here is an example usage : ...
Wno-all's user avatar
  • 1,108
2 votes
Accepted

How to reason with notations directly?

This is a general problem, not just with notations: you always have to deal with the elaborated code, not the "one you wrote". This applies to notations, but also to type-classes resolution (...
Meven Lennon-Bertrand's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible