Low* system libraries¶
KaRaMeL offers primitive support for a variety of C concepts. All new libraries
are in F*’s standard library (“ulib”) and are prefixed with
libraries found in
karamel/krmllib are being phased out and should not be
In order to abort execution of the program in a way that will always compile in
C (not trivial if you are in expression position!), look at
that will rely on either the
KRML_EABORT macro for
generating C code that compiles.
LowStar.Literal to convert string literals to immutable, always-live
buffers of uint8. This is only for dealing with literals and does not provide a
general-purpose string manipulation library.
LowStar.Printf for printing output. The
sprintf part is only for ML
code, not for Low*, unless all of the arguments to
sprintf are constants and
can be reduced into a constant string by the F* normalizer.