*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] [BUG?] value not working on an expression resulting in "True"*From*: Paolo Giarrusso <p.giarrusso at gmail.com>*Date*: Thu, 17 Apr 2008 02:14:43 +0200*User-agent*: KMail/1.9.7

Hi all, I'm a software developer and a new Isabelle user, practicing with the tutorial. I'm using Isabelle 2007. Note these two lines in the below theory (derived from § 2.5.6 of the tutorial, 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 by Ubuntu 7.04, in case it makes any difference. Thanks in advance -- "Doh!" (cit.), I've made another mistake! Paolo Giarrusso, aka Blaisorblade

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] [BUG?] value not working on an expression resulting in "True"***From:*Amine Chaieb

- Previous by Date: [isabelle] *** exception ValueMissing raised
- Next by Date: Re: [isabelle] [BUG?] value not working on an expression resulting in "True"
- Previous by Thread: Re: [isabelle] Isabelle HOL Tutorial Exercise Answers
- Next by Thread: Re: [isabelle] [BUG?] value not working on an expression resulting in "True"
- 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