Skip to content

Commit 616e04b

Browse files
authored
doc: prefer +/- for Boolean optConfig (#620)
I forgot `declare_term_config_elab` generated these for Boolean options when writing this documentation.
1 parent e3991ff commit 616e04b

2 files changed

Lines changed: 10 additions & 6 deletions

File tree

Cslib/Foundations/Data/HasFresh.lean

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -126,13 +126,13 @@ declare_term_config_elab elabFreeUnionConfig FreeUnionConfig
126126
#check free_union [f, g] ℕ
127127
128128
info: ∅ ∪ xs : Finset ℕ
129-
#check free_union (singleton := false)
129+
#check free_union -singleton ℕ
130130
131131
-- info: ∅ ∪ {x} : Finset ℕ
132-
#check free_union (finset := false)
132+
#check free_union -finset ℕ
133133
134134
-- info: ∅ : Finset ℕ
135-
#check free_union (singleton := false) (finset := false)
135+
#check free_union -singleton -finset ℕ
136136
```
137137
-/
138138
syntax (name := freeUnion) "free_union" optConfig (" [" (term,*) "]")? term : term

CslibTests/HasFresh.lean

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,17 +40,21 @@ def g (_ : String) : Finset ℕ := {4, 5, 6}
4040
#guard_msgs in
4141
#check free_union [f, g] ℕ
4242

43+
/-- info: ∅ ∪ {x} ∪ xs ∪ f var ∪ g var : Finset ℕ -/
44+
#guard_msgs in
45+
#check free_union +singleton +finset [f, g] ℕ
46+
4347
/-- info: ∅ ∪ xs : Finset ℕ -/
4448
#guard_msgs in
45-
#check free_union (singleton := false)
49+
#check free_union -singleton ℕ
4650

4751
/-- info: ∅ ∪ {x} : Finset ℕ -/
4852
#guard_msgs in
49-
#check free_union (finset := false)
53+
#check free_union -finset ℕ
5054

5155
/-- info: ∅ : Finset ℕ -/
5256
#guard_msgs in
53-
#check free_union (singleton := false) (finset := false)
57+
#check free_union -singleton -finset ℕ
5458

5559
end
5660

0 commit comments

Comments
 (0)