*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Uncaught exception in function package*From*: John Matthews <matthews at galois.com>*Date*: Thu, 22 Jul 2010 08:02:47 -0700*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4C480D95.70800@informatik.tu-muenchen.de>*References*: <473FB66C-8ECE-4E18-B370-A49B30B2070D@galois.com> <4C480D95.70800@informatik.tu-muenchen.de>

Hi Florian, Ok, that makes sense. Thanks, -john On Jul 22, 2010, at 2:21 AM, Florian Haftmann wrote:

Hi John,{-# HASKABELLE permissive mk_array #-} mk_array :: Integer -> a -> Arr a mk_array 0 x = A [] mk_array n x = A (x:xs) where xs = alist $ mk_array (n - 1) xfunction (sequential) mk_array :: "int ⇒ 'a ⇒ 'a Arr" where "mk_array 0 x = A Nil" | "mk_array n x = (let xs = alist $ mk_array (n - 1) x in A (x # xs))" sorry termination sorryThe fundamental problem is that while in Haskell overlapping patternaredisambiguated by order, in Isabelle every equations must be disambiguated "on its own" to be logically consistent andself-contained. I.e. disambiguation must be encoded syntactically.Fordatatypes this can be done using pattern disambiguation. For non-datatypes the story is not that clear (how would you encode "any number different from 0"?). Here it is perhaps best to rewrite that pattern match into an explicit if-then-else. Note that if you remove (sequential), their will be no attempt for disambiguation, but then the specification is inconsistent anyway. Hope this helps, Florian -- Home: http://www.in.tum.de/~haftmann PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
smime.p7s**

**References**:**[isabelle] Uncaught exception in function package***From:*John Matthews

**Re: [isabelle] Uncaught exception in function package***From:*Florian Haftmann

- Previous by Date: [isabelle] Isabelle tutorial view bug
- Next by Date: Re: [isabelle] Isabelle tutorial view bug
- Previous by Thread: Re: [isabelle] Uncaught exception in function package
- Next by Thread: [isabelle] paper: "Purely Functional Structured Programming" (arXiv:1007.3023)
- Cl-isabelle-users July 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list