[isabelle] not a datatype constructor err
I am a beginner in Isabelle and have faced some problems in writing a case
expression. I've defined the bellow primitives: (e and a are datatypes, S
and F are datatype constructors, and f1, f2 and g are functions)
* k = nat
e *=* S k a*|* ...
a *=* F nat *|* ...
f1 *::* "a => k"
f2 *::* "a => k"
I want to write a case expression that if e1(of type e) has the pattern "S
f1(F 0) a' " do something with a' :
case e1 of S (f1(F 0)) a' => g(a')
, but I get the "f1 is not a datatype constructor" error. How can I fix the
error? Is there another way to write the case expression (for example using
Any suggestions would be of a really great help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and