diff options
| author | Kazuhiko Sakaguchi | 2020-01-14 20:29:24 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-01-14 20:29:24 +0900 |
| commit | 85f38599f59ada198260870aa64703348e739bd8 (patch) | |
| tree | ca6b038f894769a43b865a8313585d8bda3f681e /test-suite/output/ExtractionString.out | |
| parent | 507141cb978ae9383b79e4a6af6ab968cb8d540e (diff) | |
| parent | fcc3d7c64cc3d6f8f60e0e0f9469a78009b7fbd2 (diff) | |
Merge PR #10486: [extraction] Support extraction of Coq's string type to OCaml's string type
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027
Diffstat (limited to 'test-suite/output/ExtractionString.out')
| -rw-r--r-- | test-suite/output/ExtractionString.out | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/test-suite/output/ExtractionString.out b/test-suite/output/ExtractionString.out new file mode 100644 index 0000000000..2a101d9cea --- /dev/null +++ b/test-suite/output/ExtractionString.out @@ -0,0 +1,52 @@ +(** val str : string **) + +let str = + String ((Ascii (False, False, True, False, True, False, True, False)), + (String ((Ascii (False, False, False, True, False, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, False, False, False, False, True, True, False)), + (String ((Ascii (False, False, False, False, False, True, False, False)), + (String ((Ascii (True, True, False, False, True, True, True, False)), + (String ((Ascii (False, False, True, False, True, True, True, False)), + (String ((Ascii (False, True, False, False, True, True, True, False)), + (String ((Ascii (True, False, False, True, False, True, True, False)), + (String ((Ascii (False, True, True, True, False, True, True, False)), + (String ((Ascii (True, True, True, False, False, True, True, False)), + EmptyString))))))))))))))))))))))))))))))) +str :: String +str = + String0 (Ascii False False True False True False True False) (String0 + (Ascii False False False True False True True False) (String0 (Ascii True + False False True False True True False) (String0 (Ascii True True False + False True True True False) (String0 (Ascii False False False False False + True False False) (String0 (Ascii True False False True False True True + False) (String0 (Ascii True True False False True True True False) + (String0 (Ascii False False False False False True False False) (String0 + (Ascii True False False False False True True False) (String0 (Ascii + False False False False False True False False) (String0 (Ascii True True + False False True True True False) (String0 (Ascii False False True False + True True True False) (String0 (Ascii False True False False True True + True False) (String0 (Ascii True False False True False True True False) + (String0 (Ascii False True True True False True True False) (String0 + (Ascii True True True False False True True False) + EmptyString))))))))))))))) + + +(** val str : char list **) + +let str = + 'T'::('h'::('i'::('s'::(' '::('i'::('s'::(' '::('a'::(' '::('s'::('t'::('r'::('i'::('n'::('g'::[]))))))))))))))) +(** val str : string **) + +let str = + "This is a string" +str :: Prelude.String +str = + "This is a string" + + |