| Sum.someRight c : Option Nat | |
| evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument | |
| @Sum.someRight ?m Nat c | |
| context: | |
| ⊢ Type ?u | |
| evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument | |
| @c ?m | |
| context: | |
| ⊢ Type ?u | |
| Sum.someRight c : Option Nat | |
| Sum.someRight c : Option Nat |