Re: [isabelle] Types-To-Sets: a question about further development of the framework (may be of interest to the topic Re: abelian_group)

Let me just offer my enthusiastic encouragement for you to continue!

I have never managed to figure out how Types-To-Sets can be used, despite scrutinising example developments, so you deserve full credit simply for that. It definitely needs to be made more usable.

Meanwhile the next release will contain tens of thousands of lines of new material about relativised concepts, not using Types-To-Sets but simply with new proofs ported from HOL Light. This is independent from your work, of course, but maybe the efforts can eventually be combined.


> On 13 Apr 2019, at 12:06, mailing-list anonymous <mailing.list.anonymous at> wrote:
> I would like to ask a question in relation to the further development of
> the functionality of the framework "Types-To-Sets".
> I am working on several personal projects that rely on "Types-To-Sets".
> However, as was previously noted on the mailing list, the framework does
> have its limitations. I would be interested in improving the functionality
> of the framework. However, before I do any work in this direction I would
> like to understand if anyone else is already working towards this goal and
> whether or not there exists a development plan for this framework.
> Naturally, if anyone has any particular ideas about how the framework can
> be improved, I would be interested in learning about them.

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