# Re: [isabelle] Type classes and parameters

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Type classes and parameters
• From: Esseger <esseger at free.fr>
• Date: Wed, 2 Mar 2016 22:30:46 +0100
• In-reply-to: <nanmc1$vi1$1@ger.gmane.org>
• References: <nanmc1$vi1$1@ger.gmane.org>
• User-agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:38.0) Gecko/20100101 Thunderbird/38.6.0

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.

Best,
Esseger



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