*To*: Paolo Giarrusso <p.giarrusso at gmail.com>*Subject*: Re: [isabelle] [BUG?] value not working on an expression resulting in "True"*From*: Amine Chaieb <chaieb at in.tum.de>*Date*: Thu, 17 Apr 2008 11:22:12 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200804170214.49278.p.giarrusso@gmail.com>*References*: <200804170214.49278.p.giarrusso@gmail.com>*Sender*: Amine Chaieb <chaieb.amine at googlemail.com>*User-agent*: Thunderbird 1.5.0.8 (Macintosh/20061025)

Hi,

Hope it helps, Amine. Paolo Giarrusso wrote:

Hi all, I'm a software developer and a new Isabelle user, practicing with thetutorial. I'm using Isabelle 2007.Note these two lines in the below theory (derived from Â§ 2.5.6 of thetutorial,http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf):normal_form "val (Const True)"gives:"True" :: "bool" While value "val (Const True)" (* this fails *) fails (and there are no variables, so there's no reason for this). Here's the theory: theory ExBoolexBugReport imports Main begin datatype boolex = Const bool | Neg boolex | And boolex boolex consts "val" :: "boolex \<Rightarrow> bool" primrec "val (Const b) = b" "val (Neg boolex) = (\<not> (val boolex))" "val (And b c) = ((val b) \<and> (val c))" value "True" normal_form "val (Const True)" value "val (Const True)" (* this fails *) value "val (Const (True::bool))" end Here's the error I get in the *responses* Emacs buffer. *** Error: in 'ML', line 11. *** Can't unify bool with string * Term.typ (Incompatible types) Found near *** $( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))****** Error: in 'ML', line 11.*** Can't unify Term.term with EvalTerm.Generated.boolex *** (Different type constructors) Found near *** $( Const( "ExBoolexBugReport.boolex.Const", ......), term_of_bool(x1))****** Error: in 'ML', line 14.*** Can't unify bool with string * Term.typ (Incompatible types) Found near *** $( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))****** Error: in 'ML', line 14.*** Can't unify Term.term with EvalTerm.Generated.boolex *** (Different type constructors) Found near *** $( Const( "ExBoolexBugReport.boolex.Neg", ......), term_of_boolex(x1))****** Error: in 'ML', line 19.*** Can't unify bool with string * Term.typ (Incompatible types) Found near *** $( $( Const( ...), ...(...)), term_of_boolex(x2))****** Error: in 'ML', line 19.*** Can't unify Term.term with EvalTerm.Generated.boolex *** (Different type constructors) Found near *** $( $( Const( ...), ...(...)), term_of_boolex(x2))****** At command "value".If needed: I'm using ProofGeneral-3.7pre071112 and Emacs 22.1 as provided byUbuntu 7.04, in case it makes any difference.Thanks in advance

**References**:**[isabelle] [BUG?] value not working on an expression resulting in "True"***From:*Paolo Giarrusso

- Previous by Date: [isabelle] [BUG?] value not working on an expression resulting in "True"
- Next by Date: Re: [isabelle] *** exception ValueMissing raised
- Previous by Thread: [isabelle] [BUG?] value not working on an expression resulting in "True"
- Next by Thread: [isabelle] About simplificaton
- Cl-isabelle-users April 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list