Skip to content

Commit f9e1fd7

Browse files
committed
1 parent c1ae5b3 commit f9e1fd7

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

tests/coq/test_coqtop.py

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -135,9 +135,13 @@ def test_dispatch_unicode(coq: Coqtop) -> None:
135135

136136
def test_dispatch_unprintable(coq: Coqtop) -> None:
137137
"""Should be able to handle unprintable characters."""
138-
succ, _, _, _ = coq.dispatch("Require Import String.")
138+
succ, _, _, _ = coq.dispatch("Definition parse (x : Byte.byte) : option nat := None.")
139139
assert succ
140-
succ, out, _, _ = coq.dispatch("Compute String (Ascii.ascii_of_nat 0) EmptyString.")
140+
succ, _, _, _ = coq.dispatch("Definition print (x : nat) : list Byte.byte := cons Byte.x00 nil.")
141+
assert succ
142+
succ, _, _, _ = coq.dispatch("String Notation nat parse print : nat_scope.")
143+
assert succ
144+
succ, out, _, _ = coq.dispatch("Check O.")
141145
assert succ
142146
assert "\\x00" in out
143147

0 commit comments

Comments
 (0)