Re: [isabelle] Using abbreviations with case expressions
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 don't think this is so easy. Abbreviations are unfolded only after
type inference (being typed is one of their main advantage over old
translations). Translating case expressions later would mean that the
representation that exists before that is typable in some way. This is
probably not impossible, but requires some non-trivial rethinking of how
the translation works.
In your particular example, could you just use "notation"?
This archive was generated by a fusion of
Pipermail (Mailman edition) and