| holes.lean:4:4-4:7: error: placeholders '_' cannot be used where a function is expected | |
| holes.lean:11:8-11:13: error: don't know how to synthesize placeholder | |
| context: | |
| case hole | |
| x : Nat | |
| y : Nat := g x + g x | |
| ⊢ Nat | |
| holes.lean:11:4-11:5: error: don't know how to synthesize placeholder | |
| context: | |
| x : Nat | |
| y : Nat := g x + g x | |
| ⊢ Nat | |
| holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument 'β' | |
| @g Nat (?m x) x | |
| context: | |
| x : Nat | |
| ⊢ Type | |
| holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument 'β' | |
| @g Nat (?m x) x | |
| context: | |
| x : Nat | |
| ⊢ Type | |
| holes.lean:13:10-13:11: error: failed to infer binder type | |
| holes.lean:15:16-15:17: error: failed to infer binder type | |
| holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument 'β' | |
| @f Nat (?m a) a | |
| context: | |
| a : Nat | |
| f : {α : Type} → {β : ?m a} → α → α := fun {α} {β} a => a | |
| ⊢ ?m a | |
| holes.lean:18:9-18:10: error: failed to infer binder type | |
| holes.lean:21:25-22:4: error: failed to infer definition type | |
| holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type |