2 lines
278 B
Text
2 lines
278 B
Text
bad_structures.lean:1:71: 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
|