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