mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-01 03:41:21 +00:00
Code Activity

Merge pull request #1954 from waywardmonkeys/fix-broken-link-in-docs

Browse source 
Fix broken link. It is Z3_add_rec_def, not Z3_mk_rec_def.
This commit is contained in:
Nikolaj Bjorner 2018-11-20 04:02:49 -08:00 • committed by GitHub
commit 9aaeb15d1a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/z3_api.h
View file

@ -2154,12 +2154,12 @@ extern "C" {
\param domain array containing the sort of each argument. The array must contain domain_size elements. \param domain array containing the sort of each argument. The array must contain domain_size elements.
\param range sort of the constant or the return sort of the function. \param range sort of the constant or the return sort of the function.
After declaring recursive function, it should be associated with a recursive definition #Z3_mk_rec_def. After declaring recursive function, it should be associated with a recursive definition #Z3_add_rec_def.
The function #Z3_mk_app can be used to create a constant or function The function #Z3_mk_app can be used to create a constant or function
application. application.
\sa Z3_mk_app \sa Z3_mk_app
\sa Z3_mk_rec_def \sa Z3_add_rec_def
def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT))) def_API('Z3_mk_rec_func_decl', FUNC_DECL, (_in(CONTEXT), _in(SYMBOL), _in(UINT), _in_array(2, SORT), _in(SORT)))
*/ */