michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/constants): add eq.intro

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-04 15:27:18 -08:00
parent e5381679d6
commit f0fac1ae0e
3 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/constants.cpp
View file

@ -15,6 +15,7 @@ name const * g_char = nullptr;
name const * g_char_mk = nullptr;
name const * g_dite = nullptr;
name const * g_eq = nullptr;
name const * g_eq_intro = nullptr;
name const * g_eq_rec = nullptr;
name const * g_eq_rec_eq = nullptr;
name const * g_eq_refl = nullptr;
@ -122,6 +123,7 @@ void initialize_constants() {
g_char_mk = new name{"char", "mk"};
g_dite = new name{"dite"};
g_eq = new name{"eq"};
g_eq_intro = new name{"eq", "intro"};
g_eq_rec = new name{"eq", "rec"};
g_eq_rec_eq = new name{"eq_rec_eq"};
g_eq_refl = new name{"eq", "refl"};
@ -230,6 +232,7 @@ void finalize_constants() {
delete g_char_mk;
delete g_dite;
delete g_eq;
delete g_eq_intro;
delete g_eq_rec;
delete g_eq_rec_eq;
delete g_eq_refl;
@ -337,6 +340,7 @@ name const & get_char_name() { return *g_char; }
name const & get_char_mk_name() { return *g_char_mk; }
name const & get_dite_name() { return *g_dite; }
name const & get_eq_name() { return *g_eq; }
name const & get_eq_intro_name() { return *g_eq_intro; }
name const & get_eq_rec_name() { return *g_eq_rec; }
name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
name const & get_eq_refl_name() { return *g_eq_refl; }

1
src/library/constants.h
View file

@ -17,6 +17,7 @@ name const & get_char_name();
name const & get_char_mk_name();
name const & get_dite_name();
name const & get_eq_name();
name const & get_eq_intro_name();
name const & get_eq_rec_name();
name const & get_eq_rec_eq_name();
name const & get_eq_refl_name();

1
src/library/constants.txt
View file

@ -10,6 +10,7 @@ char
char.mk
dite
eq
eq.intro
eq.rec
eq_rec_eq
eq.refl