[isabelle] Using abbreviations with case expressions
Is it unreasonable to expect this to work?
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
I suppose I could work around this problem by using something like this:
syntax emptystring :: logic ("ε")
translations "emptystring" == "CONST Nil :: string"
but the "syntax" and "translations" commands seem to be considered a
bit "old-style" nowadays, or at least a bit too low-level to be
considered best practice.
This archive was generated by a fusion of
Pipermail (Mailman edition) and