diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el
index b52d7457e..df7b16d59 100644
--- a/src/emacs/lean-syntax.el
+++ b/src/emacs/lean-syntax.el
@@ -116,7 +116,8 @@
      (,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
      ;; modifiers
      (,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[instance\]" "\[class\]" "\[parsing-only\]"
-               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[whnf\]" "\[decls\]" "\[strict\]" "\[local\]"))
+               "\[coercion\]" "\[reducible\]" "\[off\]" "\[none\]" "\[on\]" "\[wf\]" "\[whnf\]"
+               "\[decls\]" "\[strict\]" "\[local\]"))
       . 'font-lock-doc-face)
      (,(rx "\[priority" (zero-or-more (not (any "\]"))) "\]") . font-lock-doc-face)
      ;; tactics
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index f7b805b5a..4105d6d2b 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/explicit.h"
 #include "library/reducible.h"
 #include "library/coercion.h"
+#include "library/definitional/equations.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/class.h"
@@ -309,6 +310,50 @@ static void erase_local_binder_info(buffer<expr> & ps) {
         p = update_local(p, binder_info());
 }
 
+static bool is_curr_with_or_comma(parser & p) {
+    return p.curr_is_token(get_with_tk()) || p.curr_is_token(get_comma_tk());
+}
+
+expr parse_equations(parser & p, name const & n, expr const & type, buffer<expr> & auxs) {
+    buffer<expr> eqns;
+    {
+        parser::local_scope scope1(p);
+        parser::undef_id_to_local_scope scope2(p);
+        lean_assert(is_curr_with_or_comma(p));
+        expr f = mk_local(n, type);
+        if (p.curr_is_token(get_with_tk())) {
+            while (p.curr_is_token(get_with_tk())) {
+                p.next();
+                name g_name = p.check_id_next("invalid declaration, identifier expected");
+                p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
+                expr g_type = p.parse_expr();
+                expr g      = mk_local(g_name, g_type);
+                auxs.push_back(g);
+            }
+        }
+        p.check_token_next(get_comma_tk(), "invalid declaration, ',' expected");
+        p.add_local(f);
+        for (expr const & g : auxs)
+            p.add_local(g);
+        while (true) {
+            expr lhs = p.parse_expr();
+            p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
+            expr rhs = p.parse_expr();
+            eqns.push_back(mk_equation(lhs, rhs));
+            if (!p.curr_is_token(get_comma_tk()))
+                break;
+            p.next();
+        }
+    }
+    if (p.curr_is_token(get_wf_tk())) {
+        p.next();
+        expr Hwf = p.parse_expr();
+        return mk_equations(eqns.size(), eqns.data(), Hwf);
+    } else {
+        return mk_equations(eqns.size(), eqns.data());
+    }
+}
+
 // An Lean example is not really a definition, but we use the definition infrastructure to simulate it.
 enum def_cmd_kind { Theorem, Definition, Example };
 
@@ -325,6 +370,7 @@ class definition_cmd_fn {
     decl_modifiers    m_modifiers;
     name              m_real_name; // real name for this declaration
     buffer<name>      m_ls_buffer;
+    buffer<expr>      m_aux_decls;
     expr              m_type;
     expr              m_value;
     level_param_names m_ls;
@@ -361,7 +407,9 @@ class definition_cmd_fn {
             m_p.next();
             auto pos = m_p.pos();
             m_type = m_p.parse_expr();
-            if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
+            if (is_curr_with_or_comma(m_p)) {
+                m_value = parse_equations(m_p, m_name, m_type, m_aux_decls);
+            } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
                 check_end_of_theorem(m_p);
                 m_value = m_p.save_pos(mk_expr_placeholder(), pos);
             } else {
@@ -377,7 +425,9 @@ class definition_cmd_fn {
             if (m_p.curr_is_token(get_colon_tk())) {
                 m_p.next();
                 m_type = m_p.parse_scoped_expr(ps, *lenv);
-                if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
+                if (is_curr_with_or_comma(m_p)) {
+                    m_value = parse_equations(m_p, m_name, m_type, m_aux_decls);
+                } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
                     check_end_of_theorem(m_p);
                     m_value = m_p.save_pos(mk_expr_placeholder(), pos);
                 } else {
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 28ae6f39c..7145a88d5 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -86,7 +86,7 @@ void init_token_table(token_table & t) {
         {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion",
          "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]",
          "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible",
-         "evaluate", "check", "eval", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
+         "evaluate", "check", "eval", "[wf]", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude",
          "import", "inductive", "record", "structure", "module", "universe", "universes",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 629f5d96c..f602fd793 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -53,6 +53,7 @@ static name * g_on           = nullptr;
 static name * g_off          = nullptr;
 static name * g_none         = nullptr;
 static name * g_whnf         = nullptr;
+static name * g_wf           = nullptr;
 static name * g_strict       = nullptr;
 static name * g_in           = nullptr;
 static name * g_assign       = nullptr;
@@ -146,6 +147,7 @@ void initialize_tokens() {
     g_off          = new name("[off]");
     g_none         = new name("[none]");
     g_whnf         = new name("[whnf]");
+    g_wf           = new name("[wf]");
     g_strict       = new name("[strict]");
     g_in           = new name("in");
     g_assign       = new name(":=");
@@ -257,6 +259,7 @@ void finalize_tokens() {
     delete g_off;
     delete g_none;
     delete g_whnf;
+    delete g_wf;
     delete g_strict;
     delete g_ellipsis;
     delete g_fun;
@@ -333,6 +336,7 @@ name const & get_on_tk() { return *g_on; }
 name const & get_off_tk() { return *g_off; }
 name const & get_none_tk() { return *g_none; }
 name const & get_whnf_tk() { return *g_whnf; }
+name const & get_wf_tk() { return *g_wf; }
 name const & get_strict_tk() { return *g_strict; }
 name const & get_in_tk() { return *g_in; }
 name const & get_assign_tk() { return *g_assign; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index d53c73aa9..9dbf0a78d 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -55,6 +55,7 @@ name const & get_on_tk();
 name const & get_off_tk();
 name const & get_none_tk();
 name const & get_whnf_tk();
+name const & get_wf_tk();
 name const & get_strict_tk();
 name const & get_in_tk();
 name const & get_assign_tk();