Explicitly provide non-strict implicit argument

Stream: new members

[Andreas Nuyts]

Hi,
I'm coming from Agda, and the implicit argument behaviour that I'm used to, is that I can call a function f : {x : A} -> B x as either f or f {x0} or f {x = x0}.
However, in Lean, if no arguments beyond x are being supplied, this doesn't seem to work. The current code snippet I'm trying to get to work is:

Quot.ind {β = fun m => predQ (succQ m) = m}

but I get the error message "unknown identifier 'β'".
Adding @ in front as suggested in a comment here does not help:

@Quot.ind {β = fun m => predQ (succQ m) = m}

How do I get this piece of code accepted? Obviously, I cannot change the definition of Quot.ind to have strict implicit parameters.

[Aaron Liu]

Quot.ind (β := fun m => predQ (succQ m) = m)

[Etienne Marion]

The syntax is either Quot.ind (β := fun m => predQ (succQ m) = m) if you just want to specify β or @Quot.ind _ _ (fun m => predQ (succQ m) = m) if you want to make all the parameters explicit (the _ placeholders are then for the two previous argument which should be found by unification).

[Andreas Nuyts]

Oops, totally forgot about these pesky syntax differences, thank you!