blob: 12c5b202729c3bd7f060028933f2e19d58d9ee36 [file] [edit]
1371.lean:5:2-5:3: error: redundant alternative #3
1371.lean:6:2-6:3: error: redundant alternative #4