Leonardo de Moura d3eca9fa35 feat(library/type_context): improve unifier support for projections ... We need this improvement to be able to finish Section "Other goodies" described at https://github.com/leanprover/lean/wiki/Refactoring-structures Before this commit, Lean would not be able to solve constraints such as ```lean @has_add.add nat nat.has_add a b =?= @had_add.add ?A ?inst a b ``` The problem is that projections were being reduced eagerly, and the constraint would be reduced to ```lean nat.add a b =?= @had_add.add ?A ?inst a b ``` The new test proj_uniy.lean contains similar unification problems.		2017-04-27 15:55:09 -07:00
..
lean	feat(library/type_context): improve unifier support for projections	2017-04-27 15:55:09 -07:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00