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.