Gabriel Ebner 7b18d5828d feat(frontends/lean/elaborator): trigger coe_to_fun even when expected type has metavariables ... We only need to know that the expected type is a Π to perform to-function coercion. Related to #1402. Fixes https://github.com/gebner/hott3/issues/2		2017-09-06 11:20:04 +02:00
..
lean	feat(frontends/lean/elaborator): trigger coe_to_fun even when expected type has metavariables	2017-09-06 11:20:04 +02:00
.gitignore	chore(tests/lean,shell/lean): run leantests and leanruntests in parallel	2017-03-30 06:04:00 +02:00