diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index a030ed8abe..2a9e38a510 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -404,6 +404,7 @@ struct definition_info {
        Remark: a regular (i.e., safe) declaration provided by the user may contain a unsafe subexpression (e.g., tactic).
     */
     bool     m_is_unsafe{false};      // true iff current block
+    bool     m_is_partial{false};
     bool     m_is_noncomputable{false};
     bool     m_is_lemma{false};
     bool     m_aux_lemmas{false};
@@ -422,8 +423,9 @@ declaration_info_scope::declaration_info_scope(name const & ns, decl_cmd_kind ki
         info.m_actual_prefix = ns;
     }
     info.m_is_private       = modifiers.m_is_private;
-    info.m_is_unsafe_decl     = modifiers.m_is_unsafe;
-    info.m_is_unsafe          = modifiers.m_is_unsafe;
+    info.m_is_unsafe_decl   = modifiers.m_is_unsafe;
+    info.m_is_unsafe        = modifiers.m_is_unsafe;
+    info.m_is_partial       = modifiers.m_is_partial;
     info.m_is_noncomputable = modifiers.m_is_noncomputable;
     info.m_is_lemma         = kind == decl_cmd_kind::Theorem;
     info.m_aux_lemmas       = kind != decl_cmd_kind::Theorem && !modifiers.m_is_unsafe;
@@ -452,6 +454,7 @@ equations_header mk_equations_header(names const & ns, names const & actual_ns)
     h.m_fn_actual_names  = actual_ns;
     h.m_is_private       = get_definition_info().m_is_private;
     h.m_is_unsafe        = get_definition_info().m_is_unsafe;
+    h.m_is_partial       = get_definition_info().m_is_partial;
     h.m_is_noncomputable = get_definition_info().m_is_noncomputable;
     h.m_is_lemma         = get_definition_info().m_is_lemma;
     h.m_aux_lemmas       = get_definition_info().m_aux_lemmas;
diff --git a/src/library/equations_compiler/equations.cpp b/src/library/equations_compiler/equations.cpp
index d5c5139694..57c9814360 100644
--- a/src/library/equations_compiler/equations.cpp
+++ b/src/library/equations_compiler/equations.cpp
@@ -41,6 +41,7 @@ bool operator==(equations_header const & h1, equations_header const & h2) {
         h1.m_is_private == h2.m_is_private &&
         h1.m_is_lemma == h2.m_is_lemma &&
         h1.m_is_unsafe == h2.m_is_unsafe &&
+        h1.m_is_partial == h2.m_is_partial &&
         h1.m_is_noncomputable == h2.m_is_noncomputable &&
         h1.m_aux_lemmas == h2.m_aux_lemmas &&
         h1.m_prev_errors == h2.m_prev_errors &&
@@ -154,7 +155,8 @@ equations_header get_equations_header(expr const & e) {
     h.m_num_fns          = get_nat(m, name(*g_equations_name, "num_fns"))->get_small_value();
     h.m_is_private       = *get_bool(m, name(*g_equations_name, "is_private"));
     h.m_is_lemma         = *get_bool(m, name(*g_equations_name, "is_lemma"));
-    h.m_is_unsafe          = *get_bool(m, name(*g_equations_name, "is_unsafe"));
+    h.m_is_unsafe        = *get_bool(m, name(*g_equations_name, "is_unsafe"));
+    h.m_is_partial       = *get_bool(m, name(*g_equations_name, "is_partial"));
     h.m_is_noncomputable = *get_bool(m, name(*g_equations_name, "is_noncomputable"));
     h.m_aux_lemmas       = *get_bool(m, name(*g_equations_name, "aux_lemmas"));
     h.m_prev_errors      = *get_bool(m, name(*g_equations_name, "prev_errors"));
@@ -197,6 +199,7 @@ expr mk_equations(equations_header const & h, unsigned num_eqs, expr const * eqs
     m = set_bool(m, name(*g_equations_name, "is_private"), h.m_is_private);
     m = set_bool(m, name(*g_equations_name, "is_lemma"), h.m_is_lemma);
     m = set_bool(m, name(*g_equations_name, "is_unsafe"), h.m_is_unsafe);
+    m = set_bool(m, name(*g_equations_name, "is_partial"), h.m_is_partial);
     m = set_bool(m, name(*g_equations_name, "is_noncomputable"), h.m_is_noncomputable);
     m = set_bool(m, name(*g_equations_name, "aux_lemmas"), h.m_aux_lemmas);
     m = set_bool(m, name(*g_equations_name, "prev_errors"), h.m_prev_errors);
diff --git a/src/library/equations_compiler/equations.h b/src/library/equations_compiler/equations.h
index cedc88c347..5bb103d351 100644
--- a/src/library/equations_compiler/equations.h
+++ b/src/library/equations_compiler/equations.h
@@ -43,7 +43,8 @@ struct equations_header {
     names      m_fn_actual_names;         /* Full qualified name and/or private name */
     bool       m_is_private{false};       /* if true, it must be a private definition */
     bool       m_is_lemma{false};         /* if true, equations are defining a lemma */
-    bool       m_is_unsafe{false};          /* the auxiliary declarations should be tagged as unsafe */
+    bool       m_is_unsafe{false};        /* the auxiliary declarations should be tagged as unsafe */
+    bool       m_is_partial{false};       /* partial functions */
     bool       m_is_noncomputable{false}; /* if true, equation is not computable and code should not be generated */
     bool       m_aux_lemmas{false};       /* if true, we must create equation lemmas and induction principle */
     /* m_prev_errors is true when errors have already being found processing the file,