More

cvc5 · Jun 21, 2024 · bd2149f · bd2149f
1 parent 2ef4b5d
commit bd2149f
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/user_manual.md b/user_manual.md
@@ -209,7 +209,7 @@ We call `T` in the above definitions a *parameter*. The free parameters of the r
 
 ## The :requires annotation
 
-Arguments to functions can also be annotated with the attribute `:requires (<term> <term>)` to denote a condition under which the
+Arguments to functions can also be annotated with the attribute `:requires (<term> <term>)` to denote a equality condition that is required for applications of the term to type check.
 
 ```
 (declare-sort Int 0)