- md : tactic.transparency
- max_steps : ℕ
- canonize_instances : bool
- single_pass : bool
- fail_if_unchanged : bool
- eta : bool
- zeta : bool
- beta : bool
- proj : bool
- iota : bool
- unfold_reducible : bool
- memoize : bool
Instances for tactic.dsimp_config
- tactic.dsimp_config.has_sizeof_inst
- tactic.dsimp_config.inhabited
- to_dsimp_config : tactic.dsimp_config
Instances for tactic.dunfold_config
- tactic.dunfold_config.has_sizeof_inst
- tactic.dunfold_config.inhabited
Instances for tactic.delta_config
- tactic.delta_config.has_sizeof_inst
- tactic.delta_config.inhabited
- to_dsimp_config : tactic.dsimp_config
Instances for tactic.unfold_proj_config
- tactic.unfold_proj_config.has_sizeof_inst
- tactic.unfold_proj_config.inhabited
- max_steps : ℕ
- contextual : bool
- lift_eq : bool
- canonize_instances : bool
- canonize_proofs : bool
- use_axioms : bool
- zeta : bool
- beta : bool
- eta : bool
- proj : bool
- iota : bool
- iota_eqn : bool
- constructor_eq : bool
- single_pass : bool
- fail_if_unchanged : bool
- memoize : bool
- trace_lemmas : bool
Instances for tactic.simp_config
- tactic.simp_config.has_sizeof_inst
- tactic.simp_config.inhabited
- to_simp_config : tactic.simp_config
- use_hyps : bool
Instances for tactic.simp_intros_config
- tactic.simp_intros_config.has_sizeof_inst
- tactic.simp_intros_config.inhabited