From 2b749ff90d33e9793d068526f1358272808fc373 Mon Sep 17 00:00:00 2001
From: Stephen Paul Weber <singpolyma@singpolyma.net>
Date: Fri, 6 Sep 2019 20:00:13 -0500
Subject: [PATCH] Add Natural/subtract

---
 dhall-lang             |  2 +-
 lib/dhall/builtins.rb  | 17 +++++++++++++++++
 lib/dhall/typecheck.rb |  5 +++++
 3 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/dhall-lang b/dhall-lang
index f692f70..c7082d9 160000
--- a/dhall-lang
+++ b/dhall-lang
@@ -1 +1 @@
-Subproject commit f692f70bafa0322da5d9c4b535b2d323a9c5ac61
+Subproject commit c7082d910d956bcedfdc51daae989659a2db67bd
diff --git a/lib/dhall/builtins.rb b/lib/dhall/builtins.rb
index e448c17..b3563a7 100644
--- a/lib/dhall/builtins.rb
+++ b/lib/dhall/builtins.rb
@@ -98,6 +98,23 @@ module Dhall
 			end
 		end
 
+		class Natural_subtract < BuiltinFunction
+			protected
+
+			def uncurried_call(x, y)
+				if Natural_isZero.new.call(x) === true ||
+				   Natural_isZero.new.call(y) === true
+					return y
+				end
+
+				unless x.is_a?(Dhall::Natural) && y.is_a?(Dhall::Natural)
+					return unfill(x, y)
+				end
+
+				Dhall::Natural.new(value: [y.to_i - x.to_i, 0].max)
+			end
+		end
+
 		class Natural_even < BuiltinFunction
 			protected
 
diff --git a/lib/dhall/typecheck.rb b/lib/dhall/typecheck.rb
index dca5291..6dc6ba9 100644
--- a/lib/dhall/typecheck.rb
+++ b/lib/dhall/typecheck.rb
@@ -1060,6 +1060,11 @@ module Dhall
 					)
 				)
 			),
+			"Natural/subtract"  => Dhall::Forall.of_arguments(
+				Builtins[:Natural],
+				Builtins[:Natural],
+				body: Builtins[:Natural]
+			),
 			"Natural/isZero"    => Dhall::Forall.of_arguments(
 				Builtins[:Natural],
 				body: Builtins[:Bool]
-- 
2.34.2