Re: [isabelle] Unfixed variables in "define" command

Is there any context in which `define f where "f x y = …"` makes any
sense without a "for x y" afterwards?


On 22/02/2021 13:29, Makarius wrote:
> On 22/02/2021 13:26, Jakub Kądziołka wrote:
>> On Mon Feb 22, 2021 at 1:23 PM CET, Makarius wrote:
>>> Such "auto fixes" only work for toplevel specification commands, and that is
>>> already quite delicate and sometimes fragile.
>> I agree that changing the behavior could be infeasible. However, perhaps
>> it would be enough to emit a warning message when one uses 'define'
>> without 'for'?
> Warnings are generally bad design: the system needs to be strict about its
> syntax and emit proper errors.
> Within the Prover IDE, such errors could contain completion information to
> help the user get the input right, but that is quite some extra work and not
> always done.
> 	Makarius

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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