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

On 22/02/2021 14:29, Manuel Eberl wrote:
> Is there any context in which `define f where "f x y = …"` makes any
> sense without a "for x y" afterwards?

E.g. when x y are absent.

(Are you proposing special cases to complicate things?)


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