Leonardo de Moura d775ee98b4 feat(frontends/lean): auto_param support at structure_instance, and better error messages ... Summary: - A field value was being elaborated more than once when there is another field whose default value depends on it. The new test `structure_default_value_issue.lean` exposes the problem. - Better error message and localization at field type mismatches. When there is field type mismatch, the error message contains the field name, and the error is reported at the field position instead of `{`. - We add support for auto_param at structure instances `{...}` See #1422		2017-03-08 18:04:36 -08:00
..
lean	feat(frontends/lean): auto_param support at structure_instance, and better error messages	2017-03-08 18:04:36 -08:00
.gitignore	refactor(gitignore): remove old ignore entries	2016-12-10 08:42:39 -08:00