What's the equivalent of typeholes?

Stream: new members

[nrs]

In Haskell, you can use typeholes _ to get type inference from the compiler to help you write-in proper values in, e.g., function definitions. Is there an equivalent in Lean?

[Mario Carneiro]

the equivalent of _ is _

[nrs]

Mario Carneiro said:

the equivalent of _ is _

huh, am getting "don't know how to synthesize placeholder in context" in

def myfunc : Nat -> Nat
  | n => n + _

is this expected behaviour?

[Mario Carneiro]

yes, that is because you aren't done, but the error message says what type it is expecting

[nrs]

Mario Carneiro said:

yes, that is because you aren't done, but the error message says what type it is expecting

ah you're right! thanks a lot for the help!