| runTacticMustCatchExceptions.lean:2:25-2:28: error: type mismatch | |
| Iff.rfl | |
| has type | |
| ?m ↔ ?m : Prop | |
| but is expected to have type | |
| 1 ≤ a + b : Prop | |
| runTacticMustCatchExceptions.lean:3:25-3:28: error: type mismatch | |
| Iff.rfl | |
| has type | |
| ?m ↔ ?m : Prop | |
| but is expected to have type | |
| a + b ≤ b : Prop | |
| runTacticMustCatchExceptions.lean:4:25-4:28: error: type mismatch | |
| Iff.rfl | |
| has type | |
| ?m ↔ ?m : Prop | |
| but is expected to have type | |
| b ≤ 2 : Prop | |
| runTacticMustCatchExceptions.lean:9:18-9:21: error: type mismatch | |
| Iff.rfl | |
| has type | |
| ?m ↔ ?m : Prop | |
| but is expected to have type | |
| 1 ≤ a + b : Prop | |
| runTacticMustCatchExceptions.lean:10:14-10:17: error: type mismatch | |
| Iff.rfl | |
| has type | |
| ?m ↔ ?m : Prop | |
| but is expected to have type | |
| a + b ≤ b : Prop | |
| runTacticMustCatchExceptions.lean:11:14-11:17: error: type mismatch | |
| Iff.rfl | |
| has type | |
| ?m ↔ ?m : Prop | |
| but is expected to have type | |
| b ≤ 2 : Prop |