Re: [isabelle] nat_code Equation



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.