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

On 15/04/2019 12:02, Lawrence Paulson wrote:
> 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.

Recall that it is just an experiment to support a research paper in 2016
by Ondřej Kunčar and Andrei Popescu

In 2016 and 2017 I have provided a lot of concrete feedback on the
implementation to turn it into more usable state (e.g. proper use of
Isar context commands), but somehow the project seems to have become

In the meantime Fabian Immler has made some improvements, but it is
still only experimental.

Overall, there is also a high-level question about the use (or better
non-use of Types-To-Set). It is based on a genuine extension of the HOL
logic, and I am unsure what other HOL users say about it. For me this
discussion is still pending.

Meta note: I am not communicating with people that don't expose there
real name. I have just seen a bit too many recent reports about
anonymous authors doing mischief on Wikipedia.

A proper open-source project works like scientific research, by people
who stand with their own name and reputation for what they do and describe.


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