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