Dominique Unruh wrote: >> Most of our problems stem from HOL and Pure sharing a function space, >> whereas ZF has its own set theoretic one, which is of course very different >> from the Pure one. I solved this by a stratification of types into HOL/Pure >> parts, and carrying this stratification schematically through the whole >> translation process, which works because proof constants are only >> schematically polymorphic. >> > > Yes, the nice thing about Coq is that it is almost an exact superset > of what is available in HOL (at least when we use the various optional > Coq-axioms like excluded-middle and extensionality-of-equality). >
Hmm, what about typedefs? I thought they are a peculiarity of HOL and its set-theoretic model. What do they correspond to in Coq? > > > > So overall, I think the best approach for me is approach B, because it > should work well and be compatible with the current plans for the > Isabelle kernel. > Yes, it sounds like that. > Best, > Dominique >
