File tree Expand file tree Collapse file tree 1 file changed +8
-8
lines changed
Expand file tree Collapse file tree 1 file changed +8
-8
lines changed Original file line number Diff line number Diff line change 1- setLit.lean:22:19-22:21: error: overloaded, errors
1+ setLit.lean:22:19-22:21: error: overloaded, errors
22 failed to synthesize
33 EmptyCollection String
4-
4+
55 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
6-
6+
77 Fields missing: `bytes`, `isValidUTF8`
8-
8+
99 Hint: Add missing fields:
1010 ̲b̲y̲t̲e̲s̲ ̲:̲=̲ ̲_̲
11- ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲i̲s̲V̲a̲l̲i̲d̲U̲TF8̲ ̲:̲=̲ ̲_̲ ̲
12- setLit.lean:24:31-24:38: error: overloaded, errors
11+ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲ ̲i̲s̲V̲a̲l̲i̲d̲U̲T̲F̲8̲ ̲:̲=̲ ̲_̲ ̲
12+ setLit.lean:24:31-24:38: error: overloaded, errors
1313 failed to synthesize
1414 Singleton Nat String
15-
15+
1616 Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
17-
17+
1818 24:33 `val` is not a field of structure `String`
You can’t perform that action at this time.
0 commit comments