diff --git a/src/library/class.cpp b/src/library/class.cpp index 3c0d333fcf..79cf2336a0 100644 --- a/src/library/class.cpp +++ b/src/library/class.cpp @@ -473,7 +473,7 @@ list get_local_instances(type_checker & tc, list const & ctx, name c void initialize_class() { g_tmp_prefix = new name(name::mk_internal_unique_name()); - g_source = new name(*g_tmp_prefix, "source"); + g_source = new name("_source"); g_class_name = new name("classes"); g_key = new std::string("class"); class_ext::initialize(); diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index f2d4e0c0ab..239424213d 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -77,9 +77,8 @@ template class scoped_ext; typedef scoped_ext coercion_ext; void initialize_coercion() { - name p = name::mk_internal_unique_name(); - g_fun = new name(p, "Fun"); - g_sort = new name(p, "Sort"); + g_fun = new name("_Fun"); + g_sort = new name("_Sort"); g_class_name = new name("coercions"); g_key = new std::string("coerce"); coercion_ext::initialize(); diff --git a/tests/lean/852.hlean b/tests/lean/852.hlean new file mode 100644 index 0000000000..d6954c0b4c --- /dev/null +++ b/tests/lean/852.hlean @@ -0,0 +1,5 @@ +import algebra.category.functor.equivalence + +-- print prefix category.equivalence + +check @category.equivalence.to._Fun diff --git a/tests/lean/852.hlean.expected.out b/tests/lean/852.hlean.expected.out new file mode 100644 index 0000000000..ce53e0e8bf --- /dev/null +++ b/tests/lean/852.hlean.expected.out @@ -0,0 +1,6 @@ +category.equivalence.to._Fun : + Π {C : category.Precategory} {D : category.Precategory} (c : category.equivalence C D) + {a b : category.Precategory.carrier C}, + category.hom a b → + category.hom (functor.to_fun_ob (category.equivalence.to_functor c) a) + (functor.to_fun_ob (category.equivalence.to_functor c) b) diff --git a/tests/lean/binder_overload.lean.expected.out b/tests/lean/binder_overload.lean.expected.out index 56929e9dcb..d972cc0aff 100644 --- a/tests/lean/binder_overload.lean.expected.out +++ b/tests/lean/binder_overload.lean.expected.out @@ -1,7 +1,7 @@ {x : ℕ ∈ S | x > 0} : set ℕ {x : ℕ ∈ s | x > 0} : finset ℕ -@set.sep.{1} nat (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) S : set.{1} nat -@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) +@set.sep.{1} nat (λ (x : nat), @gt.{1} nat _source.to.has_lt x 0) S : set.{1} nat +@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat _source.to.has_lt x 0) (λ (a : nat), nat.decidable_lt 0 a) s : finset.{1} nat diff --git a/tests/lean/notation_priority.lean.expected.out b/tests/lean/notation_priority.lean.expected.out index cd1835f9ac..af4e2ac54c 100644 --- a/tests/lean/notation_priority.lean.expected.out +++ b/tests/lean/notation_priority.lean.expected.out @@ -1,4 +1,4 @@ -@add.{1} nat 11.source.to.has_add a b : nat -@add.{1} int 11.source.to.has_add_1 i j : int -@add.{1} nat 11.source.to.has_add a b : nat -@add.{1} int 11.source.to.has_add_1 i j : int +@add.{1} nat _source.to.has_add a b : nat +@add.{1} int _source.to.has_add_1 i j : int +@add.{1} nat _source.to.has_add a b : nat +@add.{1} int _source.to.has_add_1 i j : int diff --git a/tests/lean/pp_all.lean.expected.out b/tests/lean/pp_all.lean.expected.out index c5eae488b4..9aa2849640 100644 --- a/tests/lean/pp_all.lean.expected.out +++ b/tests/lean/pp_all.lean.expected.out @@ -1,2 +1,2 @@ a + of_num b = 10 : Prop -@eq.{1} nat (@add.{1} nat 11.source.to.has_add ((λ (x : nat), x) a) (nat.of_num 2)) 10 : Prop +@eq.{1} nat (@add.{1} nat _source.to.has_add ((λ (x : nat), x) a) (nat.of_num 2)) 10 : Prop