[isabelle] Want to auto-define datatype, predicate, & coercions given args "name", "class", & "property"



Hi,

I have a question for the Big Guns, and I posted it on Stackoverflow:

https://stackoverflow.com/questions/27865042/want-to-auto-define-with-ml-a-datatype-a-predicate-coercions-given-name

It's big enough to where I want to increase the chances that I'll either get an answer in the negative, an answer that's complete enough for me to finish it, or an answer that's a plain ole, complete working solution.

There is the UGB, the universal set of Isabelle/HOL Big Guns, and a subset of UGB, the BGAOSO, the Big Guns Active on Stackoverflow. Members of the BGAOSO have actually been very helpful, and I've gotten important answers on SO. For anything important, it seems like it was answered.

I think SO is a better staging place for a more involved question, one where there's a good chance it won't get answered, or won't get answered with enough detail for me to finish the job.

If the answer is deceptively simple, that would not be bad. Within the scope of that which is called bad, compared to that which is called good, it, a deceptively simple answer, would be of that quality which is commonly called good, or, simply, good.

It's okay if it's answered here. If it's answered here and not there, I'll probably delete the question there. I could include it all here, now, but the formatting is better there, so it seems I should leave it all there, at this time.

Thanks,
GB







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