File tree Expand file tree Collapse file tree 1 file changed +4
-4
lines changed
Expand file tree Collapse file tree 1 file changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -122,7 +122,7 @@ example (xs : List Int) (f : Int → Int) : xs.map f = xs := by
122122/--
123123info: Unable to find a counter-example
124124---
125- warning: declaration uses ' sorry'
125+ warning: declaration uses ` sorry`
126126-/
127127#guard_msgs in
128128example (a : Sum Nat Nat) : a = a := by
@@ -131,7 +131,7 @@ example (a : Sum Nat Nat) : a = a := by
131131/--
132132warning: Gave up after failing to generate values that fulfill the preconditions 100 times.
133133---
134- warning: declaration uses ' sorry'
134+ warning: declaration uses ` sorry`
135135-/
136136#guard_msgs in
137137example (a b : Sum Nat Nat) : a ≠ a → a = b := by
@@ -142,7 +142,7 @@ open Nat in
142142/--
143143info: Unable to find a counter-example
144144---
145- warning: declaration uses ' sorry'
145+ warning: declaration uses ` sorry`
146146-/
147147#guard_msgs in
148148theorem testBit_pred :
@@ -164,7 +164,7 @@ theorem type_u (α : Type u) (l : List α) : l = l ++ l := by
164164/--
165165info: Unable to find a counter-example
166166---
167- warning: declaration uses ' sorry'
167+ warning: declaration uses ` sorry`
168168-/
169169#guard_msgs in
170170theorem true_example_with_guard (a : Nat) (ha : 4 ≤ a) : a = a := by
You can’t perform that action at this time.
0 commit comments