3 lines
418 B
Text
3 lines
418 B
Text
bad_structures.lean:1:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
|
|
bad_structures.lean:4:49: error: invalid 'structure', the resultant universe must be provided when explicit universe levels are being used
|
|
bad_structures.lean:7:49: error: invalid 'structure', the resultant universe level should not be zero for any universe parameter assignment
|