Skip to content

Commit 679d2ee

Browse files
committed
fix tests
1 parent dbe98d8 commit 679d2ee

File tree

4 files changed

+7
-7
lines changed

4 files changed

+7
-7
lines changed

tests/lean/Process.lean.expected.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,6 @@
77
0
88
0
99
0
10-
"<stdin>:1:0: warning: using \'exit\' to interrupt Lean\n"
10+
"<stdin>:1:0: warning: using 'exit' to interrupt Lean\n"
1111
none
1212
some 0

tests/lean/docStr.lean.expected.out

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ doc string for 'Boo.y' is not available
1010
"Tree.node documentation "
1111
"Tree.leaf stores the values "
1212
"documenting definition in namespace "
13-
"We can document \'where\' functions too\n\n... and indentation is stripped, even after an empty line. "
13+
"We can document 'where' functions too\n\n... and indentation is stripped, even after an empty line. "
1414
doc string for 'f' is not available
1515
"let rec documentation at f "
1616
doc string for 'g' is not available

tests/lean/run/IO_test.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -85,7 +85,7 @@ info: ⟨[₂,α]⟩⟨[₂,α]⟩
8585
0
8686
"⟨[₂,α]⟩⟨[₂,α]⟩\n"
8787
1
88-
"/* Handle.getLine : Handle → IO Unit *//* The line returned by `lean_io_prim_handle_get_line` *//* is truncated at the first \'\\0\' character and the *//* rest of the line is discarded. */\n"
88+
"/* Handle.getLine : Handle → IO Unit *//* The line returned by `lean_io_prim_handle_get_line` *//* is truncated at the first '\\0' character and the *//* rest of the line is discarded. */\n"
8989
2
9090
"⟨[6,8,@]⟩\n"
9191
3

tests/lean/run/json_empty.lean

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -39,15 +39,15 @@ deriving Lean.ToJson, Lean.FromJson, Repr
3939
#eval Lean.fromJson? (α := Foo Empty) <| json% {"y": null}
4040

4141
/-! Show that parsing fails -/
42-
/-- info: Except.error "type Empty has no constructor to match JSON value \'\"Yo!\"\'.
42+
/-- info: Except.error "type Empty has no constructor to match JSON value '\"Yo!\"'.
4343
This occurs when deserializing a value for type Empty, e.g. at type Option Empty with code
44-
for the \'some\' constructor." -/
44+
for the 'some' constructor." -/
4545
#guard_msgs in
4646
#eval Lean.fromJson? (α := Empty) <| json% "Yo!"
4747

4848
/-! Show that parsing fails if we supply anything else but `null` -/
49-
/-- info: Except.error "Foo.y: type Empty has no constructor to match JSON value \'1\'.
49+
/-- info: Except.error "Foo.y: type Empty has no constructor to match JSON value '1'.
5050
This occurs when deserializing a value for type Empty, e.g. at type Option Empty with code
51-
for the \'some\' constructor." -/
51+
for the 'some' constructor." -/
5252
#guard_msgs in
5353
#eval Lean.fromJson? (α := Foo Empty) <| json% {"y": 1}

0 commit comments

Comments
 (0)