[isabelle] Want to auto-define datatype, predicate, & coercions given args "name", "class", & "property"
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: [isabelle] Want to auto-define datatype, predicate, & coercions given args "name", "class", & "property"
- From: Gottfried Barrow <igbi at gmx.com>
- Date: Fri, 09 Jan 2015 15:23:15 -0600
- User-agent: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0
I have a question for the Big Guns, and I posted it on Stackoverflow:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and