Zulip Chat Archive

Stream: general

Topic: simp_config placeholder


view this post on Zulip Sean Leather (Oct 01 2018 at 07:52):

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}

view this post on Zulip Reid Barton (Oct 01 2018 at 10:14):

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


Last updated: May 09 2021 at 20:11 UTC