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



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




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