*To*: Brian Huffman <brianh at cs.pdx.edu>*Subject*: Re: [isabelle] Using abbreviations with case expressions*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Wed, 05 Jan 2011 09:17:01 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <AANLkTimYx_KWeO-ZVvvFHx3JMqmghXtYpA_A83RMA+uZ@mail.gmail.com>*References*: <AANLkTimYx_KWeO-ZVvvFHx3JMqmghXtYpA_A83RMA+uZ@mail.gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Brian,

theory Scratch imports Main begin abbreviation (input) emptystring :: string ("ε") where "ε ≡ []" term "case s of ε ⇒ True | c # cs ⇒ False" *** Error in case expression: *** Not a datatype constructor: Scratch.emptystring *** In clause *** emptystring ⇒ True *** Failed to parse term *** At command "term" Apparently the parse translation for case expressions happens after processing notation (e.g. "[]" -> "List.Nil" or "c # cs" -> "List.Cons c cs") but before processing abbreviations (e.g. "emptystring" -> "List.Nil :: string"). Could this be changed so that abbreviations are expanded earlier?

In your particular example, could you just use "notation"? Alex

**Follow-Ups**:**Re: [isabelle] Using abbreviations with case expressions***From:*Brian Huffman

**References**:**[isabelle] Using abbreviations with case expressions***From:*Brian Huffman

- Previous by Date: Re: [isabelle] How to show that locale loop is finite?
- Next by Date: Re: [isabelle] Theory name conflict
- Previous by Thread: [isabelle] Using abbreviations with case expressions
- Next by Thread: Re: [isabelle] Using abbreviations with case expressions
- Cl-isabelle-users January 2011 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