3 files changed, 23 insertions(+), 1 deletions(-)

M dhall-lang
M lib/dhall/builtins.rb
M lib/dhall/typecheck.rb

@@ 1,1 1,1 @@
-Subproject commit f692f70bafa0322da5d9c4b535b2d323a9c5ac61
+Subproject commit c7082d910d956bcedfdc51daae989659a2db67bd

@@ 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
 

@@ 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]