2015-01-30 17:49:34 +00:00
|
|
|
|
bad_structures2.lean:7:27: error: invalid 'structure' header, field 'x' from 'boo' has already been declared with a different type
|
|
|
|
|
|
bool
|
|
|
|
|
|
and
|
2015-09-01 21:58:14 +00:00
|
|
|
|
ℕ
|
2015-01-30 17:49:34 +00:00
|
|
|
|
bad_structures2.lean:12:27: error: invalid 'structure' header, field 'x' has already been declared with a different binder annotation
|
|
|
|
|
|
bad_structures2.lean:15:1: error: field 'x' has been declared in parent structure
|
|
|
|
|
|
bad_structures2.lean:18:2: error: invalid field, identifier expected
|
|
|
|
|
|
bad_structures2.lean:23:36: error: invalid 'structure' renaming, parent structure 'foo' does not contain field 'y'
|
|
|
|
|
|
bad_structures2.lean:25:23: error: invalid 'structure' extends, 'nat' is not a structure
|
|
|
|
|
|
bad_structures2.lean:27:23: error: invalid 'structure', expression must be a 'parent' structure
|
2016-02-23 00:01:12 +00:00
|
|
|
|
bad_structures2.lean:30:0: error: failed to generate projection 'bla2.x' for 'bla2', type is an inductive predicate, but field is not a proposition
|
|
|
|
|
|
bad_structures2.lean:33:0: error: failed to generate projection 'bla3.x' for 'bla3', type is an inductive predicate, but field is not a proposition
|
