Restricted sqrt(\x:(>= 0)) <=> compute::sqrt(x)

bvssvni · May 29, 2020 · fe75724 · fe75724
1 parent 2632873
commit fe75724
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/standard_library.rs b/src/standard_library.rs
@@ -764,8 +764,8 @@ pub fn std() -> Vec<Knowledge> {
         // `mul(!\a)(\b) => mul(b)(a)`
         Red(app2(Mul, not_ret_var("a"), ret_var("b")), app2(Mul, "b", "a")),
 
-        // `sqrt(\x) <=> compute::sqrt(x)`
-        Eqv(app(Sqrt, ret_var("x")), unop_ret_var("x", Sqrt)),
+        // `sqrt(\x:(>= 0)) <=> compute::sqrt(x)`
+        Eqv(app(Sqrt, ret_pos_var("x")), unop_ret_var("x", Sqrt)),
         // `ln(\x) <=> compute::ln(x)`
         Eqv(app(Ln, ret_var("x")), unop_ret_var("x", Ln)),
         // `log2(\x) <=> compute::log2(x)`