Re: [isabelle] [BUG?] value not working on an expression resulting in "True"
- To: "Amine Chaieb" <chaieb at in.tum.de>
- Subject: Re: [isabelle] [BUG?] value not working on an expression resulting in "True"
- From: "Paolo Giarrusso" <p.giarrusso at gmail.com>
- Date: Fri, 9 May 2008 23:14:01 +0200
- Cc: isabelle-users at cl.cam.ac.uk
- In-reply-to: <480716C4.firstname.lastname@example.org>
- References: <email@example.com> <480716C4.firstname.lastname@example.org>
On Thu, Apr 17, 2008 at 11:22 AM, Amine Chaieb <chaieb at in.tum.de> wrote:
> 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.
> 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,
Paolo 'Blaisorblade' Giarrusso
This archive was generated by a fusion of
Pipermail (Mailman edition) and