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?

Manuel


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.