From 91dc9c7bd9b9c85485b68eab3a00a82a03c0c2ce Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 26 Aug 2015 13:52:53 -0700 Subject: [PATCH] fix(api): fix typos in function name and comment --- src/api/decl.cpp | 2 +- src/api/lean_env.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/decl.cpp b/src/api/decl.cpp index 23b677eef..dcf680e9d 100644 --- a/src/api/decl.cpp +++ b/src/api/decl.cpp @@ -58,7 +58,7 @@ lean_bool lean_decl_mk_thm(lean_name n, lean_list_name p, lean_expr t, lean_expr LEAN_CATCH; } -lean_bool lean_decl_mk_thm(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex) { +lean_bool lean_decl_mk_thm_with(lean_env e, lean_name n, lean_list_name p, lean_expr t, lean_expr v, lean_decl * r, lean_exception * ex) { LEAN_TRY; check_nonnull(e); check_nonnull(n); diff --git a/src/api/lean_env.h b/src/api/lean_env.h index 1f641ce07..e787a0e10 100644 --- a/src/api/lean_env.h +++ b/src/api/lean_env.h @@ -68,7 +68,7 @@ lean_bool lean_env_forget(lean_env e, lean_env * r, lean_exception * ex); \remark Every declaration passed to \c f must be disposed using \c lean_decl_del. */ lean_bool lean_env_for_each_decl(lean_env e, void (*f)(lean_decl), lean_exception * ex); /** \brief Execute \c f for each global universe in \c env. - \remark Every name passed to \c f must be disposed using \c lean_nam_del. */ + \remark Every name passed to \c f must be disposed using \c lean_name_del. */ lean_bool lean_env_for_each_univ(lean_env e, void (*f)(lean_name), lean_exception * ex); /*@}*/ /*@}*/