blob: 53c7e0ef7761b7b5788e777218ff98626302fda8 [file] [edit]
newCatPanic.lean:2:0: error: unexpected end of input; expected identifier