Re: [isabelle] Thanks Nitpick for actually answering a former, simple question



I really don't understand what you mean. Bound variables are not logical statements. And whether a variable is free or bound has no bearing on whether or not it can appear as a function's argument.

Larry Paulson


On 11 Sep 2012, at 21:07, Gottfried Barrow <gottfried.barrow at gmx.com> wrote:

> Like two months ago, I specifically asked, in a fairly precise way, "What's the difference between free variables and universally quantified variables, and is there a reason I shouldn't use free variables?"
> 
> I will now give you a reasonably close, informal, one sentence answer.
> 
> ANSWER: A universally quantified bound variable is a logical statement, where a free variable is an argument to a function.






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