Re: [isabelle] nat_code Equation
>> 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
> The ML setup in Code_Nat.thy is intended to automatically translate
> away patterns involving Suc, so that you don't have to do it yourself.
> Unfortunately the translation is kind of picky; it only works if for
> each rule with a "Suc n" pattern, there is a matching rule with a "0"
> pattern in its place.
> E.g. the following modification works with
> Code_Nat.thy in Isabelle2012:
> fun foo where
> "foo  0 = True"
> | "foo (x # xs) 0 = True"
> | "foo  (Suc _) = False"
> | "foo (x # xs) (Suc n) = foo xs n"
> But instead of changing your code, please try out the attached version
> of Code_Nat.thy, where I have modified the code preprocessor.
Thanks Brian, for the new version of Code_Nat. Unfortunately, it works for foo,
but not for other functions. A minimized example that fails is as follows:
fun double :: "nat ⇒ nat" where
"double 0 = 0"
| "double n = n + n"
export_code double in Haskell file -
Constructor as head in equation:
nat_of_num ?n ≡ plus_nat_inst.plus_nat (pred_numeral ?n) (nat_of_num num.One)
This archive was generated by a fusion of
Pipermail (Mailman edition) and