| letPatIssue.lean:3:2-3:3: error: don't know how to synthesize placeholder | |
| context: | |
| x : Nat × Nat | |
| a b : Nat | |
| ⊢ (a, b).fst + (a, b).snd ≥ 0 | |
| letPatIssue.lean:7:2-7:3: error: don't know how to synthesize placeholder | |
| context: | |
| x : Nat × Nat | |
| a b : Nat | |
| ⊢ (a, b).fst + (a, b).snd ≥ 0 | |
| letPatIssue.lean:11:2-11:6: error: unsolved goals | |
| x : Nat × Nat | |
| a b : Nat | |
| ⊢ (a, b).fst + (a, b).snd ≥ 0 | |
| letPatIssue.lean:15:2-15:6: error: unsolved goals | |
| x : Nat × Nat | |
| a b : Nat | |
| ⊢ (a, b).fst + (a, b).snd ≥ 0 | |
| letPatIssue.lean:22:2-22:6: error: unsolved goals | |
| x : Nat × Nat | |
| a b : Nat | |
| ⊢ f (a, b) > 0 |