feat(library/init): add combinators SKI

library/init/combinator.lean

@@ -0,0 +1,12 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+/- Combinator calculus -/
+namespace combinator
+definition I {A : Type} (a : A) := a
+definition K {A B : Type} (a : A) (b : B) := a
+definition S {A B C : Type} (x : A → B → C) (y : A → B) (z : A) := x z (y z)
+end combinator

library/init/default.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.datatypes init.reserved_notation init.logic
-import init.relation init.nat init.prod
+import init.relation init.nat init.prod init.combinator
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
 import init.monad init.fin init.list init.char init.string init.to_string

src/library/constants.cpp

@@ -25,6 +25,7 @@ name const * g_cast_heq = nullptr;
 name const * g_char = nullptr;
 name const * g_char_of_nat = nullptr;
 name const * g_classical = nullptr;
+name const * g_combinator_K = nullptr;
 name const * g_congr = nullptr;
 name const * g_congr_arg = nullptr;
 name const * g_congr_fun = nullptr;
@@ -324,6 +325,7 @@ void initialize_constants() {
     g_char = new name{"char"};
     g_char_of_nat = new name{"char", "of_nat"};
     g_classical = new name{"classical"};
+    g_combinator_K = new name{"combinator", "K"};
     g_congr = new name{"congr"};
     g_congr_arg = new name{"congr_arg"};
     g_congr_fun = new name{"congr_fun"};
@@ -624,6 +626,7 @@ void finalize_constants() {
     delete g_char;
     delete g_char_of_nat;
     delete g_classical;
+    delete g_combinator_K;
     delete g_congr;
     delete g_congr_arg;
     delete g_congr_fun;
@@ -923,6 +926,7 @@ name const & get_cast_heq_name() { return *g_cast_heq; }
 name const & get_char_name() { return *g_char; }
 name const & get_char_of_nat_name() { return *g_char_of_nat; }
 name const & get_classical_name() { return *g_classical; }
+name const & get_combinator_K_name() { return *g_combinator_K; }
 name const & get_congr_name() { return *g_congr; }
 name const & get_congr_arg_name() { return *g_congr_arg; }
 name const & get_congr_fun_name() { return *g_congr_fun; }

src/library/constants.h

@@ -27,6 +27,7 @@ name const & get_cast_heq_name();
 name const & get_char_name();
 name const & get_char_of_nat_name();
 name const & get_classical_name();
+name const & get_combinator_K_name();
 name const & get_congr_name();
 name const & get_congr_arg_name();
 name const & get_congr_fun_name();

src/library/constants.txt

@@ -20,6 +20,7 @@ cast_heq
 char
 char.of_nat
 classical
+combinator.K
 congr
 congr_arg
 congr_fun