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.email@example.com> <50B8D5FC.firstname.lastname@example.org> <CAAMXsiagmLap6eB1tpjB8F-Lk3DV9jeZcxvbNRNcEbO1M7NVVQ@mail.gmail.com>
> 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
Unfortunately, HOL/Library/Code_Nat.thy does not fully work in my case.
The following short example shows the problem:
fun foo where
"foo xs 0 = True"
| "foo  (Suc _) = False"
| "foo (x # xs) (Suc n) = foo xs n"
export_code foo in Haskell file -
"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.
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