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

fix(library): references to algebra in the source code

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-05 23:50:26 -08:00
parent b94e31a72c
commit 80725cc416
5 changed files with 39 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/app_builder.cpp
View file

@ -572,16 +572,16 @@ struct app_builder::imp {
expr mk_partial_left_distrib(expr const & A) {
level lvl = get_level(A);
auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_algebra_distrib_name(), {lvl}), A));
auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A));
if (!A_distrib) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_algebra_left_distrib_name(), {lvl}), A, *A_distrib);
return ::lean::mk_app(mk_constant(get_left_distrib_name(), {lvl}), A, *A_distrib);
}
expr mk_partial_right_distrib(expr const & A) {
level lvl = get_level(A);
auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_algebra_distrib_name(), {lvl}), A));
auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_distrib_name(), {lvl}), A));
if (!A_distrib) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_algebra_right_distrib_name(), {lvl}), A, *A_distrib);
return ::lean::mk_app(mk_constant(get_right_distrib_name(), {lvl}), A, *A_distrib);
}
expr mk_false_rec(expr const & c, expr const & H) {

24
src/library/constants.cpp
View file

@ -4,9 +4,9 @@
#include "util/name.h"
namespace lean{
name const * g_absurd = nullptr;
name const * g_algebra_distrib = nullptr;
name const * g_algebra_left_distrib = nullptr;
name const * g_algebra_right_distrib = nullptr;
name const * g_distrib = nullptr;
name const * g_left_distrib = nullptr;
name const * g_right_distrib = nullptr;
name const * g_add = nullptr;
name const * g_and = nullptr;
name const * g_and_elim_left = nullptr;
@ -191,9 +191,9 @@ name const * g_well_founded = nullptr;
name const * g_zero = nullptr;
void initialize_constants() {
g_absurd = new name{"absurd"};
g_algebra_distrib = new name{"algebra", "distrib"};
g_algebra_left_distrib = new name{"algebra", "left_distrib"};
g_algebra_right_distrib = new name{"algebra", "right_distrib"};
g_distrib = new name{"distrib"};
g_left_distrib = new name{"left_distrib"};
g_right_distrib = new name{"right_distrib"};
g_add = new name{"add"};
g_and = new name{"and"};
g_and_elim_left = new name{"and", "elim_left"};
@ -379,9 +379,9 @@ void initialize_constants() {
}
void finalize_constants() {
delete g_absurd;
delete g_algebra_distrib;
delete g_algebra_left_distrib;
delete g_algebra_right_distrib;
delete g_distrib;
delete g_left_distrib;
delete g_right_distrib;
delete g_add;
delete g_and;
delete g_and_elim_left;
@ -566,9 +566,9 @@ void finalize_constants() {
delete g_zero;
}
name const & get_absurd_name() { return *g_absurd; }
name const & get_algebra_distrib_name() { return *g_algebra_distrib; }
name const & get_algebra_left_distrib_name() { return *g_algebra_left_distrib; }
name const & get_algebra_right_distrib_name() { return *g_algebra_right_distrib; }
name const & get_distrib_name() { return *g_distrib; }
name const & get_left_distrib_name() { return *g_left_distrib; }
name const & get_right_distrib_name() { return *g_right_distrib; }
name const & get_add_name() { return *g_add; }
name const & get_and_name() { return *g_and; }
name const & get_and_elim_left_name() { return *g_and_elim_left; }

6
src/library/constants.h
View file

@ -6,9 +6,9 @@ namespace lean {
void initialize_constants();
void finalize_constants();
name const & get_absurd_name();
name const & get_algebra_distrib_name();
name const & get_algebra_left_distrib_name();
name const & get_algebra_right_distrib_name();
name const & get_distrib_name();
name const & get_left_distrib_name();
name const & get_right_distrib_name();
name const & get_add_name();
name const & get_and_name();
name const & get_and_elim_left_name();

6
src/library/constants.txt
View file

@ -1,7 +1,7 @@
absurd
algebra.distrib
algebra.left_distrib
algebra.right_distrib
distrib
left_distrib
right_distrib
add
and
and.elim_left

34
src/library/norm_num.cpp
View file

@ -1078,20 +1078,20 @@ void initialize_norm_num() {
g_mul_bit0 = new name("norm_num", "mul_bit0_helper");
g_mul_bit1 = new name("norm_num", "mul_bit1_helper");
g_has_mul = new name("has_mul");
g_add_monoid = new name("algebra", "add_monoid");
g_ring = new name("algebra", "ring");
g_monoid = new name("algebra", "monoid");
g_add_comm = new name("algebra", "add_comm_semigroup");
g_add_group = new name("algebra", "add_group");
g_mul_zero_class= new name("algebra", "mul_zero_class");
g_distrib = new name("algebra", "distrib");
g_add_monoid = new name("add_monoid");
g_ring = new name("ring");
g_monoid = new name("monoid");
g_add_comm = new name("add_comm_semigroup");
g_add_group = new name("add_group");
g_mul_zero_class= new name("mul_zero_class");
g_distrib = new name("distrib");
g_has_neg = new name("has_neg");
g_has_sub = new name("has_sub");
g_has_div = new name("has_div");
g_semiring = new name("algebra", "semiring");
g_lin_ord_ring = new name("algebra", "linear_ordered_ring");
g_lin_ord_semiring = new name("algebra", "linear_ordered_semiring");
g_eq_neg_of_add_eq_zero = new name("algebra", "eq_neg_of_add_eq_zero");
g_semiring = new name("semiring");
g_lin_ord_ring = new name("linear_ordered_ring");
g_lin_ord_semiring = new name("linear_ordered_semiring");
g_eq_neg_of_add_eq_zero = new name("eq_neg_of_add_eq_zero");
g_neg_add_neg_eq = new name("norm_num", "neg_add_neg_helper");
g_neg_add_pos1 = new name("norm_num", "neg_add_pos_helper1");
g_neg_add_pos2 = new name("norm_num", "neg_add_pos_helper2");
@ -1102,18 +1102,18 @@ void initialize_norm_num() {
g_sub_eq_add_neg= new name("norm_num", "sub_eq_add_neg_helper");
g_pos_add_pos = new name("norm_num", "pos_add_pos_helper");
g_neg_neg = new name("norm_num", "neg_neg_helper");
g_add_comm_group= new name("algebra", "add_comm_group");
g_add_comm_group= new name("add_comm_group");
g_add_div = new name("norm_num", "add_div_helper");
g_div_add = new name("norm_num", "div_add_helper");
g_bit0_nonneg = new name("norm_num", "nonneg_bit0_helper");
g_bit1_nonneg = new name("norm_num", "nonneg_bit1_helper");
g_zero_le_one = new name("algebra", "zero_le_one");
g_le_refl = new name("algebra", "le.refl");
g_zero_le_one = new name("zero_le_one");
g_le_refl = new name("le.refl");
g_bit0_pos = new name("norm_num", "pos_bit0_helper");
g_bit1_pos = new name("norm_num", "pos_bit1_helper");
g_zero_lt_one = new name("algebra", "zero_lt_one");
g_wk_order = new name("algebra", "weak_order");
g_field = new name("algebra", "field");
g_zero_lt_one = new name("zero_lt_one");
g_wk_order = new name("weak_order");
g_field = new name("field");
g_nonzero_neg = new name("norm_num", "nonzero_of_neg_helper");
g_nonzero_pos = new name("norm_num", "nonzero_of_pos_helper");
g_mul_div = new name("norm_num", "mul_div_helper");