Andreas Schropp wrote:
> Let me put this into perspective, in the light of a forthcoming kernel
> extension/modification:
> in this kernel patch, all sort constaints and type class reasoning
> steps are eliminated in proofterms on theorem boundaries, and strip_sorted
Sorry, I mean unconstrained variants of axioms, e.g.
OFCLASS(?'a::{}, type) ==> (?t::?'a::{})=?t
for HOL reflexivity.
> variants of the axioms are asserted on the proofterm side. So what
> remains is a proof which sort and typeclass reasoning internalized
> into the logic.
> From my POV this is needed to translate HOL into logics not involving
> Isabelle-style type classes.
