Re: [isabelle] Separation of Isabelle/Pure and Isabelle/HOL and typedef [concerning: Isabelle Foundation & Certification]

> * move typedef to Pure (which seems just to be wrong, although I have no
> example at hand for a valid Pure model that would be invalidated by that).

Well, this seems to be highly problematic to me. Coq like systems would consider
not a function space like âa => bool but âa => prop and start to build al sorts of
âsetoid constructionsâ as basis of a typeâ Meaning that complements of setoids 
do not necessarily exist.

I am afraid that any attempt to build a typedef in the Pure - Framework will
will be too special and ad-hoc for the generality that Pure adresses â

In my view, the entire construction of typedefâs makes one sense in the
context of a classical set notion (be it ZF like or HOL like).


[ â ]

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.