# [isabelle] Code_Target_Nat and threefold pattern matching

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] Code_Target_Nat and threefold pattern matching
• From: Fabian Hellauer <hellauer at in.tum.de>
• Date: Mon, 15 May 2017 14:52:56 +0200
• User-agent: Mozilla/5.0 (Windows NT 6.3; WOW64; rv:45.0) Gecko/20100101 Thunderbird/45.8.0

```Hi,

in this example

theory Scratch
imports Main "~~/src/HOL/Library/Code_Target_Nat"
begin

fun foo :: "'a list â 'a list â nat â bool" where
"foo (t#ts) (s#ss) 0 â False" |
"foo (t#ts) ss (Suc i) â False" |
"foo ts [] 0 â False" |
"foo [] ss _ â False"

export_code foo in SML

end

the code export fails with the message:
```
"Nat.zero_nat_inst.zero_nat" is not a constructor, on left hand side of equation, in theorem: foo ?ts [] zero_nat_inst.zero_nat â False
```
If I remove any of the three arguments, it works fine.
Do you have an idea what is going on?

Cheers,
Fabian
```
```theory Scratch
imports Main "~~/src/HOL/Library/Code_Target_Nat"
begin

fun foo :: "'a list \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> bool" where
"foo (t#ts) (s#ss) 0 \<longleftrightarrow> False" |
"foo (t#ts) ss (Suc i) \<longleftrightarrow> False" |
"foo ts [] 0 \<longleftrightarrow> False" |
"foo [] ss _ \<longleftrightarrow> False"

export_code foo in SML

end```

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