diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index a126575e1..cb0c52ecd 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -132,14 +132,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, nota
     optional<action> reserved_action;
     if (grp == notation_entry_group::Main) {
         if (k == mixfix_kind::prefix) {
-            if (auto at = get_reserved_nud_table(p.env()).find(tks)) {
-                reserved_pt     = at->second;
-                reserved_action = at->first;
+            if (auto ls = get_reserved_nud_table(p.env()).find(tks)) {
+                // Remark: we are ignoring multiple actions in the reserved notation table
+                reserved_pt     = head(ls).second;
+                reserved_action = head(ls).first;
             }
         } else {
-            if (auto at = get_reserved_led_table(p.env()).find(tks)) {
-                reserved_pt     = at->second;
-                reserved_action = at->first;
+            if (auto ls = get_reserved_led_table(p.env()).find(tks)) {
+                // Remark: we are ignoring multiple actions in the reserved notation table
+                reserved_pt     = head(ls).second;
+                reserved_action = head(ls).first;
             }
         }
     }
@@ -408,9 +410,11 @@ static action parse_action(parser & p, name const & prev_token, unsigned default
 static unsigned get_default_prec(optional<parse_table> const & pt, name const & tk) {
     if (!pt)
         return LEAN_DEFAULT_PRECEDENCE;
-    if (auto at = pt->find(tk)) {
-        if (at->first.kind() == notation::action_kind::Expr)
-            return at->first.rbp();
+    if (auto ls = pt->find(tk)) {
+        for (auto at : ls) {
+            if (at.first.kind() == notation::action_kind::Expr)
+                return at.first.rbp();
+        }
     }
     return LEAN_DEFAULT_PRECEDENCE;
 }
@@ -419,20 +423,22 @@ static unsigned get_default_prec(optional<parse_table> const & pt, name const &
     transition in \c pt, then return the successor table */
 static optional<parse_table> find_match(optional<parse_table> const & pt, transition const & new_trans) {
     if (pt) {
-        if (auto at = pt->find(new_trans.get_token())) {
-            if (new_trans.get_action().is_equal(at->first))
-                return optional<parse_table>(at->second);
+        if (auto ls = pt->find(new_trans.get_token())) {
+            for (auto at : ls) {
+                if (new_trans.get_action().is_equal(at.first))
+                    return optional<parse_table>(at.second);
+            }
         }
     }
     return optional<parse_table>();
 }
 
 /** \brief Lift parse_table::find method to optional<parse_table> */
-static optional<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
+static list<pair<action, parse_table>> find_next(optional<parse_table> const & pt, name const & tk) {
     if (pt)
         return pt->find(tk);
     else
-        return optional<pair<action, parse_table>>();
+        return list<pair<action, parse_table>>();
 }
 
 static unsigned parse_binders_rbp(parser & p) {
@@ -506,8 +512,9 @@ static notation_entry parse_notation_core(parser & p, bool overload, notation_en
            (grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) {
         name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default, grp);
         if (auto at = find_next(reserved_pt, tk)) {
-            action const & a = at->first;
-            reserved_pt      = at->second;
+            // Remark: we are ignoring multiple actions in the reserved notation table
+            action const & a = head(at).first;
+            reserved_pt      = head(at).second;
             switch (a.kind()) {
             case notation::action_kind::Skip:
                 if (!p.curr_is_quoted_symbol() && !p.curr_is_keyword() && !p.curr_is_token(get_assign_tk())) {
diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp
index 0a9d972db..4c47e92ee 100644
--- a/src/frontends/lean/parse_table.cpp
+++ b/src/frontends/lean/parse_table.cpp
@@ -301,9 +301,9 @@ transition replace(transition const & t, std::function<expr(expr const &)> const
 }
 
 struct parse_table::cell {
-    bool                                m_nud;
-    list<pair<unsigned, expr>>          m_accept;
-    name_map<pair<action, parse_table>> m_children;
+    bool                                      m_nud;
+    list<pair<unsigned, expr>>                m_accept;
+    name_map<list<pair<action, parse_table>>> m_children;
     MK_LEAN_RC(); // Declare m_rc counter
     void dealloc() { delete this; }
     cell(bool nud = true):m_nud(nud), m_rc(1) {}
@@ -317,12 +317,12 @@ parse_table::parse_table(parse_table && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
 parse_table::~parse_table() { if (m_ptr) m_ptr->dec_ref(); }
 parse_table & parse_table::operator=(parse_table const & s) { LEAN_COPY_REF(s); }
 parse_table & parse_table::operator=(parse_table && s) { LEAN_MOVE_REF(s); }
-optional<pair<action, parse_table>> parse_table::find(name const & tk) const {
-    auto * it = m_ptr->m_children.find(tk);
+list<pair<action, parse_table>> parse_table::find(name const & tk) const {
+    list<pair<action, parse_table>> const * it = m_ptr->m_children.find(tk);
     if (it)
-        return optional<pair<action, parse_table>>(*it);
+        return *it;
     else
-        return optional<pair<action, parse_table>>();
+        return list<pair<action, parse_table>>();
 }
 
 list<pair<unsigned, expr>> const & parse_table::is_accepting() const {
@@ -378,11 +378,12 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
             r.m_ptr->m_accept = insert(new_accept, priority, a);
         }
     } else {
-        auto * it = r.m_ptr->m_children.find(ts->get_token());
+        list<pair<action, parse_table>> const * it = r.m_ptr->m_children.find(ts->get_token());
         parse_table new_child;
         if (it) {
-            action const & act        = it->first;
-            parse_table const & child = it->second;
+            // TODO(Leo): support multiple actions
+            action const & act        = head(*it).first;
+            parse_table const & child = head(*it).second;
             if (act.is_equal(ts->get_action())) {
                 new_child = child.add_core(num-1, ts+1, a, priority, overload);
             } else {
@@ -391,7 +392,7 @@ parse_table parse_table::add_core(unsigned num, transition const * ts, expr cons
         } else {
             new_child = parse_table().add_core(num-1, ts+1, a, priority, overload);
         }
-        r.m_ptr->m_children.insert(ts->get_token(), mk_pair(ts->get_action(), new_child));
+        r.m_ptr->m_children.insert(ts->get_token(), to_list(mk_pair(ts->get_action(), new_child)));
     }
     return r;
 }
@@ -469,10 +470,12 @@ void parse_table::for_each(buffer<transition> & ts,
                                               list<pair<unsigned, expr>> const &)> const & fn) const {
     if (!is_nil(m_ptr->m_accept))
         fn(ts.size(), ts.data(), m_ptr->m_accept);
-    m_ptr->m_children.for_each([&](name const & k, pair<action, parse_table> const & p) {
-            ts.push_back(transition(k, p.first));
-            p.second.for_each(ts, fn);
-            ts.pop_back();
+    m_ptr->m_children.for_each([&](name const & k, list<pair<action, parse_table>> const & lst) {
+            for (auto const & p : lst) {
+                ts.push_back(transition(k, p.first));
+                p.second.for_each(ts, fn);
+                ts.pop_back();
+            }
         });
 }
 
@@ -713,10 +716,12 @@ static int merge(lua_State * L) {
 }
 
 static int find(lua_State * L) {
-    auto p = to_parse_table(L, 1).find(to_name_ext(L, 2));
-    if (p) {
-        push_notation_action(L, p->first);
-        push_parse_table(L, p->second);
+    list<pair<action, parse_table>> it = to_parse_table(L, 1).find(to_name_ext(L, 2));
+    if (it) {
+        // TODO(Leo): support multiple actions
+        auto p = head(it);
+        push_notation_action(L, p.first);
+        push_parse_table(L, p.second);
         return 2;
     } else {
         return push_nil(L);
diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h
index c996bb12d..e14f4718e 100644
--- a/src/frontends/lean/parse_table.h
+++ b/src/frontends/lean/parse_table.h
@@ -157,7 +157,7 @@ public:
         return add(ts.size(), ts.begin(), a, LEAN_DEFAULT_NOTATION_PRIORITY, true);
     }
     parse_table merge(parse_table const & s, bool overload) const;
-    optional<pair<action, parse_table>> find(name const & tk) const;
+    list<pair<action, parse_table>> find(name const & tk) const;
     list<pair<unsigned, expr>> const & is_accepting() const;
     void for_each(std::function<void(unsigned, transition const *, list<pair<unsigned, expr>> const &)> const & fn) const;
 
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 58df565cd..a64733075 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1086,7 +1086,8 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
         auto r = t.find(get_token_info().value());
         if (!r)
             break;
-        notation::action const & a = r->first;
+        // TODO(Leo): handle multiple actions
+        notation::action const & a = head(r).first;
         switch (a.kind()) {
         case notation::action_kind::Skip:
             next();
@@ -1214,7 +1215,7 @@ expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
             break;
         }
 
-        t = r->second;
+        t = head(r).second; // TODO(Leo):
     }
     list<pair<unsigned, expr>> const & as = t.is_accepting();
     save_overload_notation(as, p);