lean2/tests/lean/error_pos_bug.lean.expected.out

error_pos_bug.lean:9:0: error: type error in placeholder assigned to
  λ a b c,
    a
placeholder has type
  Category
but is expected to have type
  Type
the assignment was attempted when processing
    application type constraint
      Category.mk a (category.mk b c)
    term
      category.mk b c
    has type
      category a
fix(frontends/lean/elaborator): bug when reporting error position 2014-10-11 00:31:12 +00:00			`error_pos_bug.lean:9:0: error: type error in placeholder assigned to`
chore(tests): mass-update for pp.binder_types false 2016-06-01 02:14:42 +00:00			`λ a b c,`
fix(frontends/lean/elaborator): bug when reporting error position 2014-10-11 00:31:12 +00:00			`a`
			`placeholder has type`
			`Category`
			`but is expected to have type`
			`Type`
fix(kernel,library,frontends/lean): improve error messages see #669 2015-06-15 02:44:00 +00:00			`the assignment was attempted when processing`
			`application type constraint`
fix(frontends/lean/elaborator): bug when reporting error position 2014-10-11 00:31:12 +00:00			`Category.mk a (category.mk b c)`
			`term`
			`category.mk b c`
			`has type`
			`category a`