Skip to content

Commit c44d6c6

Browse files
committed
chore(Tactic/FunProp): document that config options must come before … (#35987)
…the discharger This being undocumented just bit me: let's make the documentation clearer
1 parent c106469 commit c44d6c6

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

Mathlib/Tactic/FunProp/Elab.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ documentation for `Mathlib/Tactic/FunProp.lean` for a detailed explanation.
3636
* `fun_prop [c, ...]` will unfold the constant(s) `c`, ... before decomposing `f`.
3737
* `fun_prop (config := cfg)` sets advanced configuration options using `cfg : FunProp.Config`
3838
(see `FunProp.Config` for details).
39+
These options can be combined: `fun_prop (config := cfg) (disch := tac) [c]`
3940
4041
Examples:
4142

0 commit comments

Comments
 (0)