diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2019-09-25 19:54:59 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2019-09-25 19:54:59 -0400 |
| commit | 8728f397bee2b567611dcd7a7c359c7e92159c1c (patch) | |
| tree | 283c2b659f5b9a4ed6ef097ba4b0f2052d966c28 /lib/ur/basis.urs | |
| parent | c388a91762e9dd9aef2eb097963af020c0e452f8 (diff) | |
Unicode escapes in JSON
Diffstat (limited to 'lib/ur/basis.urs')
| -rw-r--r-- | lib/ur/basis.urs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 2a98bf6f..d29bf6e6 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -95,6 +95,7 @@ val strsindex : string -> string -> option int val strcspn : string -> string -> int val substring : string -> int -> int -> string val str1 : char -> string +val ofUnicode : int -> string class show val show : t ::: Type -> show t -> t -> string |