The K Builtins (also referred to as the K Prelude or the K Standard Library)
consists of several files which contain definitions that make working with K
simpler. These files can be found under
include/kframework/builtin in your K
installation directory, and can be imported with
requires "FILENAME" (without
the path prefix).
- domains: Basic datatypes which are universally useful.
- kast: Representation of K internal data-structures (not to be included in normal definitions).
- prelude: Automatically included into every K definition.
- ffi: FFI interface for calling out to native C code from K.
- json: JSON datatype and parsers/unparsers for JSON strings.
- rat: Rational number representation.
- substitution: Hooked implementation of capture-aware sustitution for K definitions.
- unification: Hooked implementation of unification exposed directly to K definitions.