Email Gateway (Aug 19 2022 at 08:52): Email Gateway (Aug 19 2022 at 08:52):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Christian,
I reply to the easy part first, though important. The other part of your
reply is the important technical part, and I'm still thinking about that
part.
First, I'll make two general statements: (1) There's no good solution.
(2) With Isabelle, I'm out to cater to the market, however I need to do
that.
I have, at times, put a lot of thought into how I should ask code
related questions here. My short answer is usually, "Use ASCII".
Part of the problem is there are two main markets for proof assistants:
the world of mathematics and the world of computer science.
Those in the world of computer science are, by default, programmers.
Those in the world of mathematics, by and large, aren't programmers at
all, or only have basic programming skills; consequently, they can
sometimes be hostile to unsugarcoated things of a programming nature.
Trying to keep this short, I think part of my solution to catering to
the two markets is to create at least two different THYs, along with the
PDFs. But then, I can't attach 4 files to every email sent to this list.
So maybe I'll put them up somewhere on the web and provide links in the
email. I'd have to refine my scripts to create an ASCII version which
isn't completely non-verbose.
In the future, if have more suggestions about how I should give you my
code, please make those suggestions.
Regards,
GB
Last updated: Apr 18 2024 at 08:19 UTC