(*
$Id: nVCG_CaseChecker.thy 1322 2013-07-02 15:05:55Z langec $

Auction Theory Toolbox

Authors:
* Christoph Lange <math.semantic.web@gmail.com>

Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
* ISC License (1-clause BSD License)
See LICENSE file for details
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)

theory RealMinusBug
imports Main
begin

definition broken :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where "broken = (\<lambda> b n . 0::nat) - (\<lambda> b n . 0::nat)"

definition working2 :: "nat \<Rightarrow> nat"
where "working2 = (\<lambda> b . 0::nat) - (\<lambda> b . 0::nat)"

definition working1 :: "nat \<Rightarrow> nat"
where "working1 = (\<lambda> n . 0::nat) - (\<lambda> n . 0::nat)"

export_code broken in Scala
module_name RealMinusBug file "code/RealMinusBug.scala"

end