[isabelle] Code_Target_Nat and threefold pattern matching



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.