diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 890dbf621..0e4b8a975 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -55,7 +55,7 @@ "class" "parsing_only" "coercion" "unfold_full" "constructor" "reducible" "irreducible" "semireducible" "quasireducible" "wf" "whnf" "multiple_instances" "none" "decls" "declarations" - "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "congr" "backward" + "coercions" "classes" "symm" "subst" "refl" "trans" "simp" "simps" "congr" "backward" "forward" "no_pattern" "notations" "abbreviations" "begin_end_hints" "tactic_hints" "reduce_hints" "unfold_hints" "aliases" "eqv" "localrefinfo" "recursor")) diff --git a/src/library/blast/simplifier/simp_rule_set.cpp b/src/library/blast/simplifier/simp_rule_set.cpp index db2a7b394..1722b45bc 100644 --- a/src/library/blast/simplifier/simp_rule_set.cpp +++ b/src/library/blast/simplifier/simp_rule_set.cpp @@ -578,8 +578,8 @@ io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets c void initialize_simplifier_rule_set() { g_prefix = new name(name::mk_internal_unique_name()); - g_class_name = new name("rrs"); - g_key = new std::string("rrs"); + g_class_name = new name("simps"); + g_key = new std::string("simp"); rrs_ext::initialize(); } diff --git a/tests/lean/run/blast_simp_sum.lean b/tests/lean/run/blast_simp_sum.lean index 3fecca1cf..f124a239f 100644 --- a/tests/lean/run/blast_simp_sum.lean +++ b/tests/lean/run/blast_simp_sum.lean @@ -1,5 +1,5 @@ import data.nat -open - [rrs] nat +open - [simps] nat definition Sum : nat → (nat → nat) → nat := sorry