Re: [isabelle] change proposal: eliminating overloading for factorials



I would agree on not wanting to change the name of âfactâ, but not on
the syntax. Is there anything that speaks against just trying out the
â!â syntax and seeing whether anything breaks in Isabelle-dev or the
AFP? My experiments yesterday seemed to indicate that it might work.

The \<bold>! thing should work in any case. (Although, ironically,
\<bold>! looks a lot less bold than the regular ! in JEdit)

Manuel


On 02/03/15 01:02, Larry Paulson wrote:
> Personally, for the sake of compatibility and overall simplicity, Iâd prefer to leave the name of fact unchanged and certainly not try to support the (!) syntax. Renaming the theory file is not a problem, of course.
>
> Larry
>
>> On 1 Mar 2015, at 19:40, Makarius <makarius at sketis.net> wrote:
>>
>> On Sun, 1 Mar 2015, Tobias Nipkow wrote:
>>
>>>> I have nothing to add concerning overloading, just the plain name:
>>>> call it "factorial" (and the theory "Factorial") to say more clearly
>>>> what it is.
>>> I support this - provided we have a nice short syntax for "factorial", ideally the canonical "!". Maybe it is time to give up the ancient "!" syntax for \<forall>?
>> I am generally in favour of removing the old ASCII variants of well-known Pure and HOL syntax, but it will probably also take a few more years get there.  (The Prover IDE could eventually provide systematic support for this.)
>>
>> Having "!" as prefix operator (all), infix operator (nth), and postfix operator (factorial) might or might not work, depending of the chosen syntactic priorities.  Note that one also needs to consider robustness in case of bad or partial input, i.e. the potential for user confusion due to errors.
>>
>> We also have brute-force disambiguation via type-inference for tough cases, but I don't like that very much -- it has caused a lot of technical problems over the years.
>>
>>
>> A more defensive notation could use \<^bold>! instead, which is easy to type in Isabelle/jEdit, at least for people who know how to type it.
>>
>>
>> 	Makarius
>>
>





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