K Builtins

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.