lean2/tests/lean/crash.lean.expected.out

crash.lean:8:12: error: type mismatch at application
  have H' : ¬P, from H,
  ?M_1
term
  H
has type
  P
but is expected to have type
  ¬P
feat(frontends/lean): improve 'type mismatch' error position, and annotate 'have'-expressions Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-25 16:44:40 +00:00			`crash.lean:8:12: error: type mismatch at application`
feat(frontends/lean): apply eta-reduction in postprocessing step Perhaps, we should add an option to disable this new feature. Remark: this commit makes commit 46d418a redundant. I'm keeping 46d418a because we may retract this commit in the future. 2015-06-10 23:26:32 +00:00			`have H' : ¬P, from H,`
feat(frontends/lean): add 'sorry' Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-01 01:35:57 +00:00			`?M_1`
feat(kernel/error_msgs): improve application type mismatch error messages Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-28 14:08:12 +00:00			`term`
			`H`
chore(kernel/error_msgs): change type mismatch error messages, closes #33 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-07 23:18:40 +00:00			`has type`
fix(tests/lean): move crash.lean to different directory Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-07-25 15:48:35 +00:00			`P`
chore(kernel/error_msgs): change type mismatch error messages, closes #33 Signed-off-by: Leonardo de Moura <leonardo@microsoft.com> 2014-08-07 23:18:40 +00:00			`but is expected to have type`
feat(frontends/lean): apply eta-reduction in postprocessing step Perhaps, we should add an option to disable this new feature. Remark: this commit makes commit 46d418a redundant. I'm keeping 46d418a because we may retract this commit in the future. 2015-06-10 23:26:32 +00:00			`¬P`