diff --git a/project.clj b/project.clj index a3f89d0..692ec40 100644 --- a/project.clj +++ b/project.clj @@ -3,4 +3,4 @@ :dependencies [[org.clojure/clojure "1.3.0"] [match "0.2.0-SNAPSHOT"] [org.clojure/data.json "0.1.1"] - [org.clojure/core.logic "0.6.2"]]) + [org.clojure/core.logic "0.6.4"]]) diff --git a/src/logic_introduction/core.clj b/src/logic_introduction/core.clj index 9046a47..70870bf 100644 --- a/src/logic_introduction/core.clj +++ b/src/logic_introduction/core.clj @@ -20,7 +20,7 @@ ((geto exp context result-type)) ((matche [context exp result-type] ([_ [:apply ?fun ?arg] _] - (exist [arg-type] + (fresh [arg-type] (!= ?fun ?arg) (typedo context ?arg arg-type) (typedo context ?fun [arg-type :> result-type]))))))) diff --git a/src/logic_introduction/numbers.clj b/src/logic_introduction/numbers.clj index cf20cfe..51ed597 100644 --- a/src/logic_introduction/numbers.clj +++ b/src/logic_introduction/numbers.clj @@ -47,7 +47,7 @@ of x and y" (matche [x y z] ([zero _ zero]) - ([(s ?x) _ _] (exist [xy] + ([(s ?x) _ _] (fresh [xy] (times ?x y xy) (plus xy y z))))) @@ -57,7 +57,7 @@ (matche [n x y] ([(s ?x) zero zero]) ([zero (s ?x) (s zero)]) - ([(s ?n) _ _] (exist [z] + ([(s ?n) _ _] (fresh [z] (exp ?n x z) (times z x y))))) @@ -65,7 +65,7 @@ "f equals n factorial" (matche [n f] ([zero (s zero)]) - ([(s ?n) _] (exist [f1] + ([(s ?n) _] (fresh [f1] (factorial ?n f1) (times (s ?n) f1 f))))) @@ -78,7 +78,7 @@ (defn modo [x y z] "z is the remainder of the integer division of x by y" (