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



Well, even when abandoning ! as syntax for \<forall>, one could still
keep it around as a shortcut for entering â in JEdit.

There is also ALL and EX as already existing replacement ASCII syntax
for ! and ?. I usually type ALL when I want to enter â anyway; it
doesn't seem to work with EX though.

Regardless, I don't think the âforall-!â would interfere with the
ânth-!â or the âfac-!â at all due to its being a binder. So the question
of whether to adopt the âfac-!â does not necessarily depend on whether
one wants to abandon the âforall-!â.

Manuel


On 02/03/15 08:02, Tobias Nipkow wrote:
>
>
> On 01/03/2015 20:40, Makarius 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.)
>
> Well, you can already type \for to get \<forall>. Why still "!" - to
> save 3 characters?
>
> Tobias
>
>> 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.