This account is a replica from Hacker News. Its author can't see your replies. If you find this service useful, please consider supporting us via our Patreon.
| Official | https:// |
| Support this service | https://www.patreon.com/birddotmakeup |
| Official | https:// |
| Support this service | https://www.patreon.com/birddotmakeup |
Well, if you do not need to care about performance everything can be extremely simple indeed. Let me show you some data structure in coq/rocq while switching off notations and diplaying low level content.
Require Import String.
Definition hello: string := "Hello world!".
Print hello.
hello =
String (Ascii.Ascii false false false true false false true false)
(String (Ascii.Ascii true false true false false true true false)
(String (Ascii.Ascii false false true true false true true false)
(String (Ascii.Ascii false false true true false true true false)
(String (Ascii.Ascii true true true true false true true false)
(String (Ascii.Ascii false false false false false true false false)
(String (Ascii.Ascii true true true false true true true false)
(String (Ascii.Ascii true true true true false true true false)
(String (Ascii.Ascii false true false false true true true false)
(String (Ascii.Ascii false false true true false true true false)
(String
(Ascii.Ascii false false true false false true true false)
(String
(Ascii.Ascii true false false false false true false false)
EmptyString)))))))))))
: string