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

fix(library/class,library/coercion): fixes #852

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-10 22:46:17 -08:00
parent cf61adc5d5
commit 3057dde885
7 changed files with 21 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/class.cpp
View file

@ -473,7 +473,7 @@ list<expr> get_local_instances(type_checker & tc, list<expr> 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();

5
src/library/coercion.cpp
View file

@ -77,9 +77,8 @@ template class scoped_ext<coercion_config>;
typedef scoped_ext<coercion_config> 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();

5
tests/lean/852.hlean Normal file
View file

@ -0,0 +1,5 @@
import algebra.category.functor.equivalence
-- print prefix category.equivalence
check @category.equivalence.to._Fun

6
tests/lean/852.hlean.expected.out Normal file
View file

@ -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)

4
tests/lean/binder_overload.lean.expected.out
View file

@ -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

8
tests/lean/notation_priority.lean.expected.out
View file

@ -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

2
tests/lean/pp_all.lean.expected.out
View file

@ -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