Email Gateway (Aug 18 2022 at 16:28): Email Gateway (Aug 18 2022 at 16:28):From: najij mir <najim.mir@gmail.com>
Dear all,
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)
*types
datatype
e = S k a| ...
datatype
a = F nat | ...
consts
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
"if")?
Any suggestions would be of a really great help.
Kind Regards
--Mir
Email Gateway (Aug 18 2022 at 16:30):From: najij mir <najim.mir@gmail.com>
Dear all,
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)
*types
datatype
e = S k a| ...
datatype
a = F nat | ...
consts
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
"if")?
Any suggestions would be of a really great help.
Kind Regards
--Mir
Last updated: Apr 26 2024 at 20:16 UTC