From 922e66c42f76f8d71c8adab17370bdd2c673b67f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 3 Nov 2014 16:13:46 -0800
Subject: [PATCH] fix(frontends/lean/decl_cmds): do not save 'examples' in
 .ilean file

---
 src/frontends/lean/decl_cmds.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 80540a7fa..fb8c5ee68 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -486,7 +486,7 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_op
             env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, is_opaque)));
             p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
         }
-        if (!is_private)
+        if (!is_private && kind != Example)
             p.add_decl_index(real_n, n_pos, p.get_cmd_token(), type);
     }