From b5ad0fb504206e18b06b4f7163928159d1e4221f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 Nov 2014 18:37:31 -0800
Subject: [PATCH] refactor(frontends/lean/local_context): add 'const' modifier

---
 src/frontends/lean/local_context.cpp |  8 ++++----
 src/frontends/lean/local_context.h   | 10 +++++-----
 2 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/frontends/lean/local_context.cpp b/src/frontends/lean/local_context.cpp
index 3703543ce..5cc636f88 100644
--- a/src/frontends/lean/local_context.cpp
+++ b/src/frontends/lean/local_context.cpp
@@ -70,18 +70,18 @@ expr local_context::apply_context(expr const & f, tag g) const {
     return apply_context_core(f, m_ctx, g);
 }
 
-expr local_context::mk_type_metavar(name_generator & ngen, tag g) {
+expr local_context::mk_type_metavar(name_generator & ngen, tag g) const {
     name n = ngen.next();
     expr s = mk_sort(mk_meta_univ(ngen.next()), g);
     expr t = pi_abstract_context(s, g);
     return ::lean::mk_metavar(n, t, g);
 }
 
-expr local_context::mk_type_meta(name_generator & ngen, tag g) {
+expr local_context::mk_type_meta(name_generator & ngen, tag g) const {
     return apply_context(mk_type_metavar(ngen, g), g);
 }
 
-expr local_context::mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) {
+expr local_context::mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) const {
     name n      = ngen.next();
     if (suffix)
         n = n + *suffix;
@@ -90,7 +90,7 @@ expr local_context::mk_metavar(name_generator & ngen, optional<name> const & suf
     return ::lean::mk_metavar(n, t, g);
 }
 
-expr local_context::mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) {
+expr local_context::mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) const {
     expr mvar = mk_metavar(ngen, suffix, type, g);
     expr meta = apply_context(mvar, g);
     return meta;
diff --git a/src/frontends/lean/local_context.h b/src/frontends/lean/local_context.h
index 14a17657d..ffd912c9b 100644
--- a/src/frontends/lean/local_context.h
+++ b/src/frontends/lean/local_context.h
@@ -40,7 +40,7 @@ public:
            <tt>(Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u})</tt>,
         where \c ?u is a fresh universe metavariable.
     */
-    expr mk_type_metavar(name_generator & ngen, tag g);
+    expr mk_type_metavar(name_generator & ngen, tag g) const;
 
     /** \brief Assuming \c m_ctx is
            <tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@@ -50,7 +50,7 @@ public:
 
         \remark The type of the resulting expression is <tt>Type.{?u}</tt>
     */
-    expr mk_type_meta(name_generator & ngen, tag g);
+    expr mk_type_meta(name_generator & ngen, tag g) const;
 
     /** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
            <tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@@ -64,7 +64,7 @@ public:
 
         \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
     */
-    expr mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g);
+    expr mk_metavar(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) const;
 
     /** \brief Given <tt>type[l_1, ..., l_n]</tt> and assuming \c m_ctx is
            <tt>[l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ]</tt>,
@@ -75,8 +75,8 @@ public:
 
         \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name.
     */
-    expr mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g);
-    expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g) {
+    expr mk_meta(name_generator & ngen, optional<name> const & suffix, optional<expr> const & type, tag g) const;
+    expr mk_meta(name_generator & ngen, optional<expr> const & type, tag g) const {
         return mk_meta(ngen, optional<name>(), type, g);
     }