Email Gateway (Aug 17 2022 at 13:45): Email Gateway (Aug 17 2022 at 13:45):From: Primrose.Mbanefo@Infineon.com
Hi,
Could someone please tell me what is wrong with:
consts sortL2 :: "int list ⇒ int list"
primrec
"sortL2 [] = []"
"sortL2 (x#xs) = (case xs of [] ⇒ [x] | y # ys ⇒ (if (x < y) then (y#(sortL2 (x#(ys)))) else (x#(sortL2 (y#ys))))) "
No matter how I turn it I either get a type unification error or a constant defined on RHS error.
Thanks for your time.
Primrose
Email Gateway (Aug 17 2022 at 13:45):From: nipkow@in.tum.de
"sortL2 (x#xs) = (case xs of [] $B"M(J [x] | y # ys $B"M(J (if (x < y) then (y#(sortL2 (x#(ys)))) else (x#(sortL2 (y#ys))))) "
is not primrec: you are only allowed recursive calls sortL2 xs. The tutorial
describves the primrec requirement in detail. Your function must be defined
with recdef.
Tobias
PS Please try to stick to ascii in your emails.
Email Gateway (Aug 17 2022 at 13:45):From: Primrose.Mbanefo@Infineon.com
Sorry about the non-ascii symbols. I forgot to check the mail before I
sent it.
I am trying to prove some lemmas about list sorting (I tried to
implement a kind of bubble sort)
But I can't. could I send the files to any one to look at?
Thanks
Primrose
Last updated: May 03 2024 at 04:19 UTC