10 lines
312 B
Text
10 lines
312 B
Text
error_loc_bug.lean:74:17: error: type mismatch at application
|
||
weakening2 (OrI₁ Γ A B H)
|
||
term
|
||
OrI₁ Γ A B H
|
||
has type
|
||
Γ ⊢ A ∨ B
|
||
but is expected to have type
|
||
Γ ⊢ ⌞A ∧ B⌟
|
||
The following identifier(s) are introduced as free variables by the left-hand-side of the equation:
|
||
Γ A B Δ H Hs
|