Email Gateway (Aug 18 2022 at 09:45): Email Gateway (Aug 18 2022 at 09:45):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello,
I'm writing a function to contruct a list of given length.
I defined a datatype:
datatype resource = free | taken
and the function:
emptyRes2aux :: "unit => nat => resource list"
primrec
"emptyRes2aux () (k) = (case k of 0 => [] | Suc h => free # emptyRes2aux ()
h)"
The first question is: why now Isabelle give me the error:
*** Constant to be defined occurs on rhs
*** The error(s) above occurred in definition "emptyRes2aux_unit_def":
*** "emptyRes2aux == unit_rec (nat_case [] (h::nat. free # emptyRes2aux ()
h))"
*** At command "primrec".
?
Second question: if I don't use unit and () in the definition of the
function, why Isabelle return the error:
*** Primrec definition error:
*** constructor missing
*** in
*** "emptyRes2aux (k::nat) = (case k of 0 => [] | Suc (h::nat) => free #
emptyRes2aux h)"
*** At command "primrec".
?
Thanks
Gabriele
Email Gateway (Aug 18 2022 at 09:45):From: Tobias Nipkow <nipkow@in.tum.de>
Isabelle complains about missing constructors because the constructors
0/Suc should occur on the lhs. Please read the description and the many
examples of primrec in the tutorial.
Tobias
Email Gateway (Aug 18 2022 at 09:45):From: Tjark Weber <tjark.weber@gmx.de>
Gabriele,
what you want to define seems to be equal to
replicate n free
(See HOL/List.thy for the definition of "replicate".)
Best,
Tjark
Email Gateway (Aug 18 2022 at 09:45):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Hello,
I tried to use the constructors only in the left hand (how I read in the
tutorial) but Isabelle tell me that there are many non-variable terms in
lhs.
However I resolved the problem using recdef.
Thanks and best regards
Gabriele
Email Gateway (Aug 18 2022 at 09:46):From: Gabriele Pozzani <gabriele.pozzani@gmail.com>
Oops...I read List.thy but I don't seen it.
Sorry.
Thanks
Gabriele
Last updated: May 03 2024 at 08:18 UTC