4 lines
123 B
Text
4 lines
123 B
Text
858.lean:2:18: error: don't know how to synthesize placeholder
|
|
context:
|
|
⊢ Sort ?
|
|
858.lean:2:18: error: elaborator failed
|