Re: [isabelle] [BUG?] value not working on an expression resulting in "True"

On Thu, Apr 17, 2008 at 11:22 AM, Amine Chaieb <chaieb at> wrote:
> Hi,

> The problem appears to be with the constructor "Const" which is the same
> name as the constructor "Const" for internal represaentation of Lambda terms
> in Isabelle.

> Your theory works if you change Const into Cst.

Yes, indeed.

> Maybe the Code generator
> should rename such constants before emitting ML Code for evaluation?

Sorry for the late answer, but I thought that having a separate
namespace altogether for all user-defined symbols could be nicer. Or
Anyway, is anybody working on a fix for this in the code?

> Hope it helps,
> Amine.

Paolo 'Blaisorblade' Giarrusso

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