5 lines
351 B
Text
5 lines
351 B
Text
inductive_sorry.lean:1:0: error: type of parameter 'A' contains 'sorry'
|
|
inductive_sorry.lean:4:0: error: type of parameter 'foo' contains 'sorry'
|
|
inductive_sorry.lean:7:0: error: constructor 'foo.mk' contains 'sorry'
|
|
inductive_sorry.lean:10:0: error: type of parameter 'A' contains 'sorry'
|
|
inductive_sorry.lean:12:0: error: field 'x' contains 'sorry'
|