lean2/tests/lean/red.lean.expected.out

red.lean:9:19: error: type mismatch at definition 'example', has type
  f = f
but is expected to have type
  f = g
red.lean:12:0: error: type mismatch at application
  eq.subst H rfl
term
  rfl
has type
  f ?M_1 = f ?M_1
but is expected to have type
  f ?M_1 = a
red.lean:17:0: error: type mismatch at application
  eq.subst H rfl
term
  rfl
has type
  f ?M_1 = f ?M_1
but is expected to have type
  f ?M_1 = a
feat(frontends/lean/decl_cmds): avoid funny names when displaying error messages for "examples" 2015-06-01 22:35:28 +00:00			`red.lean:9:19: error: type mismatch at definition 'example', has type`
feat(frontends/lean): add '[semireducible]' attribute This commit also renames the elements of reducible_status. The idea is to use in the C++ implementation the same names used in the Lean front-end. 2015-03-03 18:48:36 +00:00			`f = f`
			`but is expected to have type`
			`f = g`
			`red.lean:12:0: error: type mismatch at application`
			`eq.subst H rfl`
			`term`
			`rfl`
			`has type`
			`f ?M_1 = f ?M_1`
			`but is expected to have type`
			`f ?M_1 = a`
			`red.lean:17:0: error: type mismatch at application`
			`eq.subst H rfl`
			`term`
			`rfl`
			`has type`
			`f ?M_1 = f ?M_1`
			`but is expected to have type`
			`f ?M_1 = a`