simp_config placeholder

Stream: general

[Sean Leather]

I just discovered this by accident:

example : ℕ := by simp _

error: don't know how to synthesize placeholder
context:
⊢ opt_param tactic.simp_config_ext
    {to_simp_config := {max_steps := simp.default_max_steps,
                        contextual := ff,
                        lift_eq := tt,
                        canonize_instances := tt,
                        canonize_proofs := ff,
                        use_axioms := tt,
                        zeta := tt,
                        beta := tt,
                        eta := tt,
                        proj := tt,
                        iota := tt,
                        iota_eqn := ff,
                        constructor_eq := tt,
                        single_pass := ff,
                        fail_if_unchanged := tt,
                        memoize := tt},
     discharger := tactic.failed unit}

[Reid Barton]

Nice! rw [] _ also works to see rw options.