Skip to content

Commit

Permalink
chore: more test file formatting cleanup
Browse files Browse the repository at this point in the history
  • Loading branch information
thorimur committed Sep 12, 2023
1 parent efd52f6 commit a32f7d7
Showing 1 changed file with 14 additions and 1 deletion.
15 changes: 14 additions & 1 deletion test/tryThis.lean
Original file line number Diff line number Diff line change
Expand Up @@ -43,12 +43,15 @@ elab "add_suggestions" s:term "with_header" h:term : tactic => unsafe do

/-- Demo adding a suggestion. -/
macro "#demo1" s:term : command => `(example : True := by add_suggestion $s; trivial)

/-- Demo adding a suggestion with a header. -/
macro "#demo1" s:term "with_header" h:term : command => `(example : True := by
add_suggestion $s with_header $h; trivial)

/-- Demo adding suggestions. -/
macro "#demo" s:term : command => `(example : True := by
add_suggestions $s; trivial)

/-- Demo adding suggestions with a header. -/
macro "#demo" s:term "with_header" h:term : command => `(example : True := by
add_suggestions $s with_header $h; trivial)
Expand Down Expand Up @@ -76,7 +79,8 @@ Try these:
• rfl
• rfl
```
with `rfl` in text-link color/ -/
with `rfl` in text-link color.
-/
#demo #[s,s,s,s]

/-
Expand Down Expand Up @@ -150,6 +154,15 @@ info: We've got everything here! Such as:
#guard_msgs in
#demo #[s,s,s,s] with_header "We've got everything here! Such as:"

/--
info: Grab bag:
• not a tactic
• This
• rfl
• link-styled
• this
-/
#guard_msgs in
#demo #[
{s with
suggestion := "not a tactic",
Expand Down

0 comments on commit a32f7d7

Please sign in to comment.