3 lines
148 B
Text
3 lines
148 B
Text
@test1 : {α : Sort u_2} → α → Sort u_1
|
||
levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry'
|
||
@test2 : {α : Sort u_2} → α → Sort u_1
|