From aaad9a3c43c8efeca357d6e554f4bb9641f9fa3c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 31 Oct 2014 13:03:29 -0700
Subject: [PATCH] feat(library/definitional/projection): add option for marking
 main premise as instance implicit (i.e., `[]` binder decorator)

---
 src/library/definitional/projection.cpp | 9 +++++----
 src/library/definitional/projection.h   | 4 ++--
 2 files changed, 7 insertions(+), 6 deletions(-)

diff --git a/src/library/definitional/projection.cpp b/src/library/definitional/projection.cpp
index 6347008091..937bd1f50b 100644
--- a/src/library/definitional/projection.cpp
+++ b/src/library/definitional/projection.cpp
@@ -45,7 +45,7 @@ static bool is_prop(expr type) {
     return is_sort(type) && is_zero(sort_level(type));
 }
 
-environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names) {
+environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit) {
     // Given an inductive datatype C A (where A represent parameters)
     //   intro : Pi A (x_1 : B_1[A]) (x_2 : B_2[A, x_1]) ..., C A
     //
@@ -73,7 +73,8 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
         params.push_back(param);
     }
     expr C_A                     = mk_app(mk_constant(n, lvls), params);
-    expr c                       = mk_local(ngen.next(), name("c"), C_A, binder_info());
+    binder_info c_bi             = inst_implicit ? mk_inst_implicit_binder_info() : binder_info();
+    expr c                       = mk_local(ngen.next(), name("c"), C_A, c_bi);
     buffer<expr> intro_type_args; // arguments that are not parameters
     expr it = intro_type;
     while (is_pi(it)) {
@@ -132,7 +133,7 @@ static name mk_fresh_name(environment const & env, buffer<name> const & names, n
     }
 }
 
-environment mk_projections(environment const & env, name const & n) {
+environment mk_projections(environment const & env, name const & n, bool inst_implicit) {
     auto p  = get_nparam_intro_rule(env, n);
     unsigned num_params = p.first;
     inductive::intro_rule ir = p.second;
@@ -145,6 +146,6 @@ environment mk_projections(environment const & env, name const & n) {
         i++;
         type = binding_body(type);
     }
-    return mk_projections(env, n, proj_names);
+    return mk_projections(env, n, proj_names, inst_implicit);
 }
 }
diff --git a/src/library/definitional/projection.h b/src/library/definitional/projection.h
index 5e956ad70f..73af63718d 100644
--- a/src/library/definitional/projection.h
+++ b/src/library/definitional/projection.h
@@ -8,6 +8,6 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
-environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names);
-environment mk_projections(environment const & env, name const & n);
+environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit = false);
+environment mk_projections(environment const & env, name const & n, bool inst_implicit = false);
 }