| 243.lean:2:10-2:14: error: application type mismatch | |
| ⟨Bool, true⟩ | |
| argument | |
| true | |
| has type | |
| _root_.Bool : Type | |
| but is expected to have type | |
| Bool : Type | |
| 243.lean:13:7-13:8: error: application type mismatch | |
| ⟨A, a⟩ | |
| argument | |
| a | |
| has type | |
| Foo.A : Type | |
| but is expected to have type | |
| A : Type |