Skip to content

Commit

Permalink
docs
Browse files Browse the repository at this point in the history
  • Loading branch information
@artie2000
artie2000 committed Jan 22, 2025
1 parent f417d87 commit 631cd40
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Tactic/SetLike.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ so we must put this declaration into its own file.
declare_aesop_rule_sets [SetLike] (default := true)
declare_aesop_rule_sets [SetLike!] (default := false)

library_note "SetLike Aesop lemmas"/--
library_note "SetLike Aesop ruleset"/--
The Aesop tactic (`aesop`) can automatically prove obvious facts about membership in structures
such as subgroups and subrings. Certain lemmas regarding membership in algebraic substructures
are given the `aesop` attribute according to the following principles:
Expand Down

0 comments on commit 631cd40

Please sign in to comment.