Re: [isabelle] Type classes and parameters

Maybe I wasn't clear enough that the only problem I have is that the Banach spaces depend on a parameter. A similar question would arise when defining for instance the L^p spaces, for p in [1, \infty) (maybe the most prominent missing block in Multivariate_Analysis).

Does the absence of answer mean that there is no nice way to do this in current Isabelle, and that tools with dependent type theory such as CoQ would be better suited for the task? That would be very sad in my opinion, as Isar is by far more mathematician-friendly, and the analysis libraries are also by far superior in Isabelle/HOL.


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