# Re: [isabelle] nat_code Equation

*To*: Brian Huffman <huffman at in.tum.de>, Isabelle Users <isabelle-users at cl.cam.ac.uk>
*Subject*: Re: [isabelle] nat_code Equation
*From*: René Thiemann <rene.thiemann at uibk.ac.at>
*Date*: Mon, 3 Dec 2012 10:18:50 +0100
*In-reply-to*: <CAAMXsiagmLap6eB1tpjB8F-Lk3DV9jeZcxvbNRNcEbO1M7NVVQ@mail.gmail.com>
*References*: <FB64BADF-227D-4ED8-988B-57680C25BB73@uibk.ac.at> <50B8CDE9.3070807@in.tum.de> <50B8D5FC.8040009@in.tum.de> <CAAMXsiagmLap6eB1tpjB8F-Lk3DV9jeZcxvbNRNcEbO1M7NVVQ@mail.gmail.com>

Hi Brian,
> Note that if you import HOL/Library/Code_Nat.thy, which declares a
> binary code representation for type nat, then the implementation of
> function nat from Code_Integer is *much* faster than either nat' or
> nat_th.
Unfortunately, HOL/Library/Code_Nat.thy does not fully work in my case.
The following short example shows the problem:
theory Test
imports "~~/src/HOL/Library/Code_Nat"
begin
fun foo where
"foo xs 0 = True"
| "foo [] (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"
export_code foo in Haskell file -
complains about
"Nat.Suc" is not a constructor, on left hand side of equation, in theorem:
foo [] (Suc ?uu) ≡ False
Of course, I can drop the pattern matching on Suc, but I do not want to do that
manually for all my functions.
Cheers,
René
PS: The problem also occurs in the development version of Isabelle where
I imported Code_Binary_Nat instead of Code_Nat (changeset ad52ddd35c3a)
--
René Thiemann mailto:rene.thiemann at uibk.ac.at
Computational Logic Group http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science phone: +43 512 507-6434
University of Innsbruck

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*