More tests

Author: robsimmons

tests/lean/run/idSuggestStandalone.lean

@@ -23,7 +23,7 @@ error: Invalid field `test0`: The environment does not contain `String.test0`, s
 of type `String`
 
 Hint: Perhaps you meant `String.foo` in place of `String.test0`:
-  "abc".t̵e̵s̵t̵0̵f̲o̲o̲
+  .t̵e̵s̵t̵0̵f̲o̲o̲
 -/
 #guard_msgs in
 #check "abc".test0
@@ -44,8 +44,8 @@ error: Invalid field `test1`: The environment does not contain `String.test1`, s
 of type `String`
 
 Hint: Perhaps you meant one of these in place of `String.test1`:
-  [apply] `String.foo`: "abc".foo
-  [apply] `String.baz`: "abc".baz
+  [apply] `String.foo`
+  [apply] `String.baz`
 -/
 #guard_msgs in
 #check "abc".test1
@@ -67,9 +67,9 @@ error: Invalid field `test2`: The environment does not contain `String.test2`, s
 of type `String`
 
 Hint: Perhaps you meant one of these in place of `String.test2`:
-  [apply] `String.foo`: "abc".foo
-  [apply] `String.baz`: "abc".baz
-  [apply] `String.bar`: "abc".bar
+  [apply] `String.foo`
+  [apply] `String.baz`
+  [apply] `String.bar`
 -/
 #guard_msgs in
 #check "abc".test2
@@ -119,7 +119,7 @@ error: Invalid field `toNum`: The environment does not contain `Foo.Bar.toNum`,
 of type `Foo.Bar`
 
 Hint: Perhaps you meant `Foo.Bar.toNat` in place of `Foo.Bar.toNum`:
-  Foo.Bar.three.t̵o̵N̵u̵m̵t̲o̲N̲a̲t̲
+  .t̵o̵N̵u̵m̵t̲o̲N̲a̲t̲
 -/
 #guard_msgs in
 #eval Foo.Bar.three.toNum
@@ -130,7 +130,7 @@ error: Invalid field `toStr`: The environment does not contain `Foo.Bar.toStr`,
 of type `Foo.Bar`
 
 Hint: Perhaps you meant `Foo.Bar.toString` in place of `Foo.Bar.toStr`:
-  Foo.Bar.two.t̵o̵S̵t̵r̵t̲o̲S̲t̲r̲i̲n̲g̲
+  .t̵o̵S̵t̵r̵t̲o̲S̲t̲r̲i̲n̲g̲
 -/
 #guard_msgs in
 #eval Foo.Bar.two.toStr
@@ -274,7 +274,35 @@ error: Invalid field `not`: The environment does not contain `MyBool.not`, so it
 of type `MyBool`
 
 Hint: Perhaps you meant `MyBool.swap` in place of `MyBool.not`:
-  MyBool.tt.n̵o̵t̵s̲w̲a̲p̲
+  .n̵o̵t̵s̲w̲a̲p̲
 -/
 #guard_msgs in
 example := MyBool.tt.not
+
+/--
+error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
+  (fun x => if x < 3 then MyBool.tt else MyBool.ff) 4
+of type `MyBool`
+
+Hint: Perhaps you meant `MyBool.swap` in place of `MyBool.not`:
+  .n̵o̵t̵s̲w̲a̲p̲
+-/
+#guard_msgs in
+example := ((fun x => if x < 3 then MyBool.tt else .ff) 4).not
+
+
+@[suggest_for MyBool.not]
+def MyBool.justFalse : MyBool → MyBool
+  | _ => ff
+
+/--
+error: Invalid field `not`: The environment does not contain `MyBool.not`, so it is not possible to project the field `not` from an expression
+  (fun x => if x < 3 then MyBool.tt else MyBool.ff) 4
+of type `MyBool`
+
+Hint: Perhaps you meant one of these in place of `MyBool.not`:
+  [apply] `MyBool.justFalse`
+  [apply] `MyBool.swap`
+-/
+#guard_msgs in
+example := ((fun x => if x < 3 then MyBool.tt else .ff) 4).not