Leonardo de Moura
|
85f7132efe
|
feat(frontends/lean/placeholder_elaborator): perform class-instance resolution in a completely independent unifier object, it also triggers the resolution when expected type does not contain metavariables, closes #175, closes #173, closes #68
|
2014-09-11 14:49:35 -07:00 |
|
Leonardo de Moura
|
80fd14b39e
|
refactor(frontends/lean): replace collect_metavars with metavar_closure helper class
|
2014-09-11 14:49:35 -07:00 |
|
Leonardo de Moura
|
6bc41f8dde
|
refactor(frontends/lean/elaborator): move placeholder_elaborator to its own module
|
2014-09-10 16:42:49 -07:00 |
|