### Example: Generate Lean 4 Project from K Definition

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/klean/README.md

Demonstrates the process of compiling a K definition and then using `klean` to generate a Lean 4 project. Assumes Lean 4 and K Framework are installed and configured.

```bash
$ kompile src/tests/integration/test-data/k-files/imp.k  # kompile the IMP definition
$ uv run klean imp-kompiled klean-imp                # generate the Lean 4 project
```

--------------------------------

### Install K Framework with Nix

Source: https://github.com/runtimeverification/k/blob/master/README.md

Installs the K Framework using Nix, a streamlined process for users not developing K. It first fetches an installation script and then uses the 'kup' tool to install K.

```shell
bash <(curl https://kframework.org/install)
kup install k
```

--------------------------------

### GDB: Start and Step Through K Rewrites

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/19_debugging/README.md

This section provides examples of using GDB commands to debug K programs. It illustrates how to start the program and break before the first rewrite step ('k start'), and how to execute single or multiple rewrite steps ('k step').

```gdb
Temporary breakpoint 1 at 0x239210
Starting program: /home/dwightguth/kframework-5.0.0/k-distribution/k-tutorial/1_basic/19_debugging/lesson-19-a-kompiled/interpreter .krun-2021-08-13-14-10-50-sMwBkbRicw/tmp.in.01aQt85TaA -1 .krun-2021-08-13-14-10-50-sMwBkbRicw/result.kore
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib/x86_64-linux-gnu/libthread_db.so.1".

Temporary breakpoint 1, 0x0000000000239210 in main () 
0x0000000000231890 in step (subject=<k>
  0 ~> .
</k>)
(gdb)
```

```gdb
Continuing.

Temporary breakpoint -22, 0x0000000000231890 in step (subject=<k>
  1 ~> .
</k>)
(gdb)
```

```gdb
Continuing.

Temporary breakpoint -23, 0x0000000000231890 in step (subject=<k>
  11 ~> .
</k>)
(gdb)
```

--------------------------------

### Compile and Run K Tutorial Example

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/INSTALL.md

Illustrates the process of compiling a K language definition and running a sample program using `make kompile` and `krun`. This verifies the K toolchain's functionality with a simple factorial example.

```sh
cd pl-tutorial/2_languages/1_simple/1_untyped
make kompile
krun tests/diverse/factorial.simple
```

--------------------------------

### K: Kompile Command Example

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/05_modules/README.md

This is an example of how to compile a multi-file K definition using the 'kompile' command. It specifies the entry point file 'colorOf.k'.

```bash
kompile colorOf.k

```

--------------------------------

### Run Programs with krun

Source: https://github.com/runtimeverification/k/blob/master/README.md

Example of how to execute a program using the 'krun' command. It assumes that the 'k-distribution/target/release/k/bin' directory is in the system's PATH.

```bash
krun <program_file>
```

--------------------------------

### K Definition Example: lesson-19-d.k

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/19_debugging/README.md

A sample K definition illustrating syntax for Foo, Bar, and Baz, including a rule labeled 'baz'. This serves as an example for demonstrating rule matching.

```k
module LESSON-19-D

  syntax Foo ::= foo(Bar)
  syntax Bar ::= bar(Baz) | bar2(Baz)
  syntax Baz ::= baz() | baz2()

  rule [baz]: foo(bar(baz())) => .K

endmodule
```

--------------------------------

### Compile Definitions with kompile

Source: https://github.com/runtimeverification/k/blob/master/README.md

Example of how to compile K definitions using the 'kompile' command. It assumes that the 'k-distribution/target/release/k/bin' directory is in the system's PATH.

```bash
kompile <definition_directory>
```

--------------------------------

### K Set Operations Examples

Source: https://context7.com/runtimeverification/k/llms.txt

Showcases operations on unordered sets in K, emphasizing fast membership testing. Includes examples for creation, union, intersection, difference, size, subset checking, and conversions to/from lists.

```k
module SET-EXAMPLES
  imports SET
  imports INT

  syntax Set ::= demo() [function]

  // Create sets
  rule demo() => SetItem(1) SetItem(2) SetItem(3)

  // Empty set
  rule demo() => .Set

  // Set union (duplicate elements merged automatically)
  rule demo() => SetItem(1) SetItem(2) SetItem(2)  // => SetItem(1) SetItem(2)

  // Set membership
  rule demo() => 2 in (SetItem(1) SetItem(2))  // => true

  // Set intersection
  rule demo() => intersectSet(SetItem(1) SetItem(2), SetItem(2) SetItem(3))
       // => SetItem(2)

  // Set difference
  rule demo() => SetItem(1) SetItem(2) -Set SetItem(2)  // => SetItem(1)

  // Set size
  rule demo() => size(SetItem(1) SetItem(2))  // => 2

  // Subset check
  rule demo() => SetItem(1) <=Set SetItem(1) SetItem(2)  // => true

  // Convert list to set (removes duplicates)
  rule demo() => List2Set(ListItem(1) ListItem(2) ListItem(1))
       // => SetItem(1) SetItem(2)

  // Convert set to list
  rule demo() => Set2List(SetItem(1) SetItem(2))
       // => ListItem(1) ListItem(2) (order unspecified)

endmodule

```

--------------------------------

### Clone K PL Tutorial

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/INSTALL.md

Provides the command to clone the K PL Tutorial repository. This is the first step in testing K packages by setting up a local environment with example K languages and programs.

```sh
git clone https://www.github.com/runtimeverification/pl-tutorial
```

--------------------------------

### Install Build Dependencies (Debian/Ubuntu/macOS)

Source: https://github.com/runtimeverification/k/blob/master/README.md

Installs build and runtime dependencies for the K Framework on Debian-based systems (like Ubuntu) or macOS with Homebrew. This script simplifies the prerequisite installation process.

```shell
./install-build-deps
```

--------------------------------

### K Tutorial: IMP Language Definition

Source: https://github.com/runtimeverification/k/blob/master/web/toc.md

Guides on defining the IMP language using K, focusing on syntax, configuration, and computational rules.

```k
-- Example K definition for IMP language would go here.
```

--------------------------------

### Starting the kserver (Blocking)

Source: https://github.com/runtimeverification/k/blob/master/docs/ktools.md

Command to start the kserver in blocking mode, useful for quick testing. The server runs in the same process and shares threads, reducing startup time and resource contention.

```sh
kserver
```

--------------------------------

### Starting the kserver (Non-blocking)

Source: https://github.com/runtimeverification/k/blob/master/docs/ktools.md

Command to start the kserver in non-blocking mode, suitable for automation. Logs are directed to a specified file.

```sh
spawn-kserver <log.flie>
```

--------------------------------

### lakefile.toml Configuration for Lean Project

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/klean/README.md

Example `lakefile.toml` for a Lean 4 project generated by `klean`. It defines the project name, version, default targets, weak Lean arguments, and specifies the Lean library.

```toml
# klean-imp/lakefile.toml

name = "klean-imp"
version = "0.1.0"
defaultTargets = ["KleanImp"]
weakLeanArgs = [
    "-D maxHeartbeats=10000000"
]

[[lean_lib]]
name = "KleanImp"
```

--------------------------------

### Python Project Setup with pyproject.toml

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/kdist/README.md

Defines a Python project's metadata, build system requirements, and dependencies, including 'kframework'. This configuration is essential for using tools like 'uv' and enabling entry points for kdist.

```toml
[build-system]
requires = ["hatchling"]
build-backend = "hatchling.build"

[project]
name = "imp-semantics"
version = "0.1.0"
description = "K semantics for a simple imperative programing language"
readme = "README.md"
requires-python = "~=3.10"
dependencies = [
    "kframework",
]

[[project.authors]]
name = "Runtime Verification, Inc."
email = "contact@runtimeverification.com"

```

--------------------------------

### Basic K Module Syntax

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/05_modules/README.md

Defines a basic K module structure. Modules are the fundamental unit for grouping K sentences. This example shows an empty module.

```k
module LESSON-05-A

endmodule
```

--------------------------------

### K Substring Extraction Examples

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/10_strings/README.md

Demonstrates the 'substrString' function in K for extracting substrings. The examples show how to get the first 5 characters and all characters from the 3rd position onwards.

```k
substrString(S, 0, 5)
substrString(S, 3, lengthString(S))
```

--------------------------------

### K Proof Environment Skeleton

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/22_proofs/README.md

A skeleton K code snippet to set up the proof environment. It imports necessary modules like 'lesson-22.k' and 'domains.md', and defines modules for syntax and verification.

```k
requires "lesson-22.k"
requires "domains.md"

module LESSON-22-SPEC-SYNTAX
    imports LESSON-22-SYNTAX

endmodule

module VERIFICATION
    imports K-EQUAL
    imports LESSON-22-SPEC-SYNTAX
    imports LESSON-22
    imports MAP-SYMBOLIC

endmodule

module LESSON-22-SPEC
    imports VERIFICATION

endmodule

```

--------------------------------

### K Tutorial: LAMBDA Syntax and Commands

Source: https://github.com/runtimeverification/k/blob/master/web/toc.md

Introduction to defining the LAMBDA language in K, covering basic syntax, modules, and fundamental K commands.

```k
-- Example K definition for LAMBDA syntax would go here.
```

--------------------------------

### K Default Priority Example

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

Highlights the default priority assignment in K, where rules without explicit priority attributes are assigned a priority of 50. This is demonstrated with an example combining default and 'owise' rules.

```k
syntax Int ::= foo(Int) [function]
rule foo(0) => 0 [priority(50)]
rule foo(_) => 1 [owise]
```

--------------------------------

### K Definition for Debugging Example

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/19_debugging/README.md

A simple K language definition that increments an integer until it reaches 100. This serves as an example program to be compiled and debugged.

```k
module LESSON-19-A
  imports INT

  rule I => I +Int 1
    requires I <Int 100
endmodule

```

--------------------------------

### K Syntax Examples: Rule Matching and State Update

Source: https://github.com/runtimeverification/k/blob/master/src/front-end-requirements.txt

Illustrates the desired concrete syntax for K rules, showcasing pattern matching with variables and function calls. This syntax is intended to be more readable and maintainable than its parenthesized equivalent.

```k
rule <k> X=V => V ...</k>  <state>...X|->(_=>V)...</state>
rule <k> print(I,Xs => Xs) ...</k> <out>... .=>I </out>
```

--------------------------------

### K Definition Example

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/19_debugging/README.md

This K definition includes syntax for a boolean function 'isBlue' and fruit types, along with rules for their evaluation. It serves as an example for setting breakpoints.

```k
module LESSON-19-B
  imports BOOL

  syntax Bool ::= isBlue(Fruit) [function]
  syntax Fruit ::= Blueberry() | Banana()
  rule isBlue(Blueberry()) => true
  rule isBlue(Banana()) => false

  rule F:Fruit => isBlue(F)
endmodule

```

--------------------------------

### K Tutorial: IMP++ Language Extensions

Source: https://github.com/runtimeverification/k/blob/master/web/toc.md

Explains how to extend the IMP language to IMP++ using K, covering configuration refinement, tagging, and semantic lists.

```k
-- Example K definition for IMP++ would go here.
```

--------------------------------

### Kompile and Krun Commands for LESSON-02-B

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/02_basics/README.md

Commands to compile the K definition LESSON-02-B and then run it with a specific program. Uses the '--definition' flag to specify the compiled definition.

```bash
kompile lesson-02-b.k
krun -cPGM='colorOf(Banana())' --definition 'lesson-02-b-kompiled'
```

--------------------------------

### K Anonymous Function Application Example 2

Source: https://github.com/runtimeverification/k/wiki/New-Features

An example illustrating an anonymous function applied to a term returned by `someFunctionReturningVal()`. The function checks if the bound variable `V` satisfies two boolean conditions using `isFoo` and `isBar`.

```k
#fun(V::Val => isFoo(V) andBool isBar(V))(someFunctionReturningVal())
```

--------------------------------

### K Anonymous Function Application Example 1

Source: https://github.com/runtimeverification/k/wiki/New-Features

An example demonstrating the use of anonymous functions to match a record pattern and bind its fields to a variable 'K', implicitly passing 'Record' as an argument. This showcases how K can be captured from the outer scope.

```k
foo(K, Record) => #fun(record(... field: _ => K))(Record)
```

--------------------------------

### Kompile and Krun Commands for LESSON-02-C

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/02_basics/README.md

Commands to compile the K definition LESSON-02-C and then run it with a specific program. Uses the '--definition' flag to specify the compiled definition.

```bash
kompile lesson-02-c.k
krun -cPGM='colorOf(Banana())' --definition 'lesson-02-c-kompiled'
```

--------------------------------

### Time Retrieval

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/tests/profiling/test-data/domains.md

Gets the current system time.

```APIDOC
## Time Retrieval

### Description
Retrieves the current system time as seconds since the Unix epoch.

### Method
N/A (K function)

### Endpoint
N/A (K function)

### Parameters
None

### Request Example
```k
#time()
```

### Response
#### Success Response
- **Int** - The current time in seconds since January 1, 1970, UTC.

#### Response Example
```k
// Returns the current time as an integer, e.g., 1678886400
```
```

--------------------------------

### File Position Management

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/tests/profiling/test-data/domains.md

Provides functions to get the current file position and to set the file position.

```APIDOC
## File Position Management

### Description
Manage the current position within an opened file.

### Method
N/A (K functions)

### Endpoint
N/A (K functions)

### Parameters
#### Path Parameters
- **fd** (Int) - Required - The file descriptor.
- **index** (Int) - Required - The desired file offset for `#seek`.
- **fromEnd** (Int) - Required - Offset from the end of the file for `#seekEnd`.

### Request Example
```k
#tell(fd)
#seek(fd, 100)
#seekEnd(fd, -50) // Seek 50 bytes from the end
```

### Response
#### Success Response
- **IOInt** (`#tell`) - The current file offset.
- **K** (`#seek`, `#seekEnd`) - `.K` on success.

#### Response Example
```k
// #tell returns an integer offset, e.g., 100
// #seek and #seekEnd return .K on success
```
```

--------------------------------

### Dockerfile Base Image for K

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/INSTALL.md

Shows how to use a K framework Docker image as a base for your own Dockerfile. This allows you to build custom images with K pre-installed, simplifying your build process.

```dockerfile
FROM runtimeverificationinc/kframework-k:ubuntu-jammy-COMMIT_ID
```

--------------------------------

### Introduce Symbolic Integer

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/21_symbolic_execution/README.md

This K rule shows how to introduce a fresh symbolic integer variable '?X' into the configuration. When this rule is applied, a new variable is created and then unified against subsequent rules for symbolic execution.

```k
rule <k> foo => ?X:Int ...</k>
```

--------------------------------

### Get Length of Bytes in K

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/tests/profiling/test-data/domains.md

Returns the length of a Bytes object in O(1) time. This is a total function.

```k
syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)]
```

--------------------------------

### Compile K Definition

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/02_basics/README.md

This command compiles a K definition file (`.k`) into an executable definition that can be used by `krun`. It prepares the K program for execution.

```bash
kompile lesson-02-d.k
```

--------------------------------

### Run K Docker Image

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/INSTALL.md

Demonstrates how to execute a K framework Docker image directly from the command line. This is useful for interactive sessions or running K commands within a containerized environment.

```sh
docker run -it runtimeverificationinc/kframework-k:ubuntu-jammy-COMMIT_ID
```

--------------------------------

### K Simplification Rule Example

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

Demonstrates a K rule with the 'simplification' attribute, illustrating how function arguments can be nested on the left-hand side, which is not allowed in function definition rules.

```k
rule (X +Int Y) +Int Z => X +Int (Y +Int Z) [simplification]
```

--------------------------------

### K Tutorial: Type Systems Definition

Source: https://github.com/runtimeverification/k/blob/master/web/toc.md

Demonstrates defining imperative, environment-based type systems within the K framework.

```k
-- Example K definition for type systems would go here.
```

--------------------------------

### Adding kdist Entry Point to pyproject.toml

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/kdist/README.md

Configures the project's entry points to expose kdist plugins. This allows kdist to discover and load custom build targets defined within the project.

```toml
[project.entry-points.kdist]
imp-semantics = "imp_semantics.kdist.plugin"

```

--------------------------------

### K: Get Set Size (Cardinality)

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md

Retrieves the number of elements (cardinality) within a Set. This operation has a time complexity of O(1).

```k
syntax Int ::= size(Set)                [function, total, hook(SET.size)]
```

--------------------------------

### Compile and Execute K Program with Variables

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/02_basics/README.md

This sequence of commands first compiles a K definition (`lesson-02-e.k`) and then executes a program using `krun`. The execution demonstrates how the variable `F` in the rule captures and returns the matched `Fruit`.

```bash
kompile lesson-02-e.k 
krun -cPGM='contentsOfJar(Jar(Apple()))' --definition 'lesson-02-e-kompiled'
```

--------------------------------

### Handle Ambiguity with Brackets in K

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/03_parsing/README.md

Demonstrates parsing a boolean expression with the logical AND and OR operators, which can lead to parsing ambiguity. The example shows the error message resulting from this ambiguity in the 'and-or.bool' file.

```k
true && false || false
```

--------------------------------

### Run K Framework Test Suite with Maven

Source: https://github.com/runtimeverification/k/blob/master/README.md

Command to run the complete test suite for the K Framework using Maven. This includes unit tests, checkstyle, and the 'ktest' execution.

```bash
mvn verify
```

--------------------------------

### Get Map Values as List (K)

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md

Retrieves all values from a map as a List. This operation has a time complexity of O(N). Uses the MAP.values hook.

```k
syntax List ::= values(Map)                   [function, hook(MAP.values)]
```

--------------------------------

### K Program Definition: LESSON-02-A

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/02_basics/README.md

Defines syntax for colors and fruits, and a function 'colorOf' that maps fruits to colors. This is a basic K definition file compiled using 'kompile'. It requires no external dependencies.

```k
module LESSON-02-A

  syntax Color ::= Yellow() | Blue()
  syntax Fruit ::= Banana() | Blueberry()
  syntax Color ::= colorOf(Fruit) [function]

  rule colorOf(Banana()) => Yellow()
  rule colorOf(Blueberry()) => Blue()

endmodule

```

--------------------------------

### Get Map Keys as List (K)

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md

Retrieves all keys from a map as a List. This operation has a time complexity of O(N). Uses the MAP.keys_list hook.

```k
syntax List ::= "keys_list" "(" Map ")"       [function, hook(MAP.keys_list)]
```

--------------------------------

### Build K Framework with Nix

Source: https://github.com/runtimeverification/k/blob/master/README.md

Command to build the K Framework project using Nix flakes. This command compiles the project and its dependencies, placing a link to the resulting binaries in the 'result/' folder. It's recommended to set up a binary cache for faster builds.

```bash
nix build .
```

--------------------------------

### Get Map Keys as Set (K)

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md

Retrieves all keys from a map as a Set. This operation has a time complexity of O(N). Uses the MAP.keys hook.

```k
syntax Set ::= keys(Map)                      [function, total, hook(MAP.keys)]
```

--------------------------------

### GDB/LLDB Debugging with K

Source: https://github.com/runtimeverification/k/blob/master/docs/ktools.md

Demonstrates setting breakpoints and stepping through K execution using GDB. LLDB is used on macOS. Requires `--debugger` flag with `krun` and specific GDB/LLDB initialization for K term pretty-printing. Note: GDB syntax is shown, LLDB commands may differ.

```gdb
(gdb) break definition.kore:k_step
Breakpoint 1 at 0x25e340
(gdb) run
Breakpoint 1, 0x000000000025e340 in step (subject=`<generatedTop>{}`(`<k>{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("0", "Int")),dotk{}(.KList))),`<generatedCounter>{}`(#token("0", "Int"))))
(gdb) continue
Continuing.

Breakpoint 1, 0x000000000025e340 in step (subject=`<generatedTop>{}`(`<k>{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("1", "Int")),dotk{}(.KList))),`<generatedCounter>{}`(#token("0", "Int"))))
(gdb) continue 2
Will ignore next crossing of breakpoint 1.  Continuing.

Breakpoint 1, 0x000000000025e340 in step (subject=`<generatedTop>{}`(`<k>{}`(`kseq{}`(`inj{Int{}, KItem{}}`(#token("3", "Int")),dotk{}(.KList))),`<generatedCounter>{}`(#token("0", "Int"))))
(gdb) 
```

--------------------------------

### Fix JAVA_HOME Environment Variable

Source: https://github.com/runtimeverification/k/blob/master/README.md

Ensures the JAVA_HOME environment variable points to the correct JDK installation directory, not the JRE. This is crucial for build tools that rely on Java.

```shell
export JAVA_HOME=/path/to/your/jdk
```

--------------------------------

### K Syntax with Location Attributes

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

Example of defining K syntax with the 'locations' attribute to include file, line, and column metadata in the parse tree. This allows for more precise error reporting and debugging.

```k
syntax Exp [locations]
  syntax Exp ::= Exp "/" Exp | Int
```

--------------------------------

### K Module Importing Another Module

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/05_modules/README.md

Shows how one K module can import sentences from another. 'LESSON-05-D-1' defines boolean syntax, and 'LESSON-05-D' imports it and defines the 'not' rules.

```k
module LESSON-05-D-1
  syntax Boolean ::= "true" | "false"
  syntax Boolean ::= "not" Boolean [function]
endmodule

module LESSON-05-D
  imports LESSON-05-D-1

  rule not true => false
  rule not false => true
endmodule
```

--------------------------------

### K: Projection Cast Usage Example

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

Demonstrates the projection cast in action. It shows how the result of 'foo(I +Int 1)', which returns 'Exp', is projected to 'Int' to be used as an argument for the 'bar' function.

```k
syntax Exp ::= foo(Exp) [function] | bar(Int) | Int
rule foo(I:Int) => I
rule bar(I) => bar({foo(I +Int 1)}:>Int)
```

--------------------------------

### K Parser Ambiguity Error Message

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md

An example of a parsing ambiguity error message generated by the K parser. It lists the possible interpretations of the ambiguous input, showing the differing AST structures.

```text
[Error] Inner Parser: Parsing ambiguity.
1: syntax Stmt ::= "if" "(" Exp ")" Stmt
    `if(_)__LESSON-04-E_Stmt_Exp_Stmt`(
      `true_LESSON-04-E_Exp`(.KList),
      `if(_)_else__LESSON-04-E_Stmt_Exp_Stmt_Stmt`(
        `false_LESSON-04-E_Exp`(.KList),
        `{}_LESSON-04-E_Stmt`(.KList),
        `{}_LESSON-04-E_Stmt`(.KList)
      )
    )

2: syntax Stmt ::= "if" "(" Exp ")" Stmt "else" Stmt
    `if(_)_else__LESSON-04-E_Stmt_Exp_Stmt_Stmt`(
      `true_LESSON-04-E_Exp`(.KList),
      `if(_)__LESSON-04-E_Stmt_Exp_Stmt`(
        `false_LESSON-04-E_Exp`(.KList),
        `{}_LESSON-04-E_Stmt`(.KList)
      ),
      `{}_LESSON-04-E_Stmt`(.KList)
    )

	Source(./dangling-else.if)
	Location(1,1,1,32)
	1 |	if (true) if (false) {} else {}
	  .	^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
```

--------------------------------

### Kprove: Prove with Claims and Custom Backend Options

Source: https://context7.com/runtimeverification/k/llms.txt

Demonstrates how to use kprove to verify specifications using specific claim labels or custom Haskell backend arguments. Requires `kprove` and a `.k` specification file.

```python
from kprove import kprove
from pathlib import Path

# Prove with specific claims
result = kprove.prove(
    spec_file=Path('spec.k'),
    claim_labels=['addition-commutative', 'multiplication-associative']
)

# Prove with custom backend options
result = kprove.prove(
    spec_file=Path('spec.k'),
    haskell_backend_args=[
        '--log-level', 'debug',
        '--smt-timeout', '500'
    ]
)
```

--------------------------------

### K Semantics: L-value and Map Range Operations

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md

Defines K semantics for 'lvalue' to get the location of an identifier and for map range operations to manage key-value pairs within a specified range.

```k
syntax Exp ::= lvalue(K)
  syntax Val ::= loc(Int)

  rule <k> lvalue(X:Id => loc(L)) ...</k> <env>... X |-> L:Int ...</env>

  context lvalue(_::Exp[HOLE::Exps])
  context lvalue(HOLE::Exp[_::Exps])

  rule lvalue(lookup(L:Int) => loc(L))


  syntax Map ::= Int "..." Int "|->" K [function]
  rule N...M |-> _ => .Map  requires N >Int M
  rule N...M |-> K => N |-> K (N +Int 1)...M |-> K  requires N <=Int M
```

--------------------------------

### K Auxiliary Operations: Declarations, Lookup, and Environment Setup

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/tests/regression-new/pl-tutorial/2_languages/2_kool/1_untyped/kool-untyped.md

Provides K semantics for auxiliary operations: 'mkDecls' for variable declarations, 'lookup' to retrieve values from a store, and 'setEnv' to update the environment.

```k
syntax Stmt ::= mkDecls(Ids,Vals)  [function]
  rule mkDecls((X:Id, Xs:Ids), (V:Val, Vs:Vals)) => var X=V; mkDecls(Xs,Vs)
  rule mkDecls(.Ids,.Vals) => {}

  syntax Exp ::= lookup(Int)
  rule <k> lookup(L) => V ...</k> <store>... L |-> V:Val ...</store>  [group(lookup)]

  syntax KItem ::= setEnv(Map)
  rule <k> setEnv(Env) => .K ...</k>  <env> _ => Env </env>
  rule (setEnv(_) => .K) ~> setEnv(_)
```

--------------------------------

### K Language: Marking Symbols as Deprecated

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

This example illustrates how to use the `deprecated` attribute in K to mark symbols that are obsolete. The compiler will issue a warning if a deprecated symbol is used in a rule, context, or configuration.

```k
syntax Foo ::= foo() [deprecated]
rule foo() => . // warning on this line
```

--------------------------------

### Build Lean Project with lake

Source: https://github.com/runtimeverification/k/blob/master/pyk/src/pyk/klean/README.md

Command to build the generated Lean 4 project using `lake`. It shows the output messages during the build process, including manifest creation and toolchain updates.

```bash
$ lake -d klean-imp build
info: klean-imp: no previous manifest, creating one from scratch
info: toolchain not updated; already up-to-date
Build completed successfully.
```

--------------------------------

### FUN Language: Currying Desugaring Example

Source: https://github.com/runtimeverification/k/blob/master/pyk/regression-new/pl-tutorial/2_languages/3_fun/1_untyped/1_environment/fun-untyped.md

Demonstrates how multiple space-separated arguments in FUN functions and let/letrec binders are desugared into single-argument functions using currying.

```K
```
fun x y -> x y
```

are desugared into the following expressions:

```
fun x -> fun y -> x y
```
```

```K
```
let x y = y in x
```

are desugared into the following expressions:

```
let x = fun y -> y in x
```
```

--------------------------------

### K Module with Configuration Variables for Inputs

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/15_configurations/README.md

A K module that compares two integers. It declares '<k>', '<first>', and '<second>' cells. '<first>' and '<second>' are initialized via configuration variables '$FIRST' and '$SECOND', respectively. The '<k>' cell is empty.

```k
module LESSON-15-B-SYNTAX
  imports INT-SYNTAX
endmodule

module LESSON-15-B
  imports LESSON-15-B-SYNTAX
  imports INT
  imports BOOL

  configuration <k> . </k>
                <first> $FIRST:Int </first>
                <second> $SECOND:Int </second>

  rule <k> . => FIRST >Int SECOND </k>
       <first> FIRST </first>
       <second> SECOND </second>
endmodule
```

--------------------------------

### LLDB: Launch Interpreter and Set Arguments

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/19_debugging/README.md

This snippet demonstrates how to launch the K interpreter using LLDB on macOS and set runtime arguments. It includes commands for creating the target, importing debug scripts, and configuring run arguments.

```lldb
(lldb) target create "./lesson-19-a-kompiled/interpreter"
warning: 'interpreter' contains a debug script. To run this script in this debug session:

    command script import "/Users/brucecollie/code/scratch/lesson-19-a-kompiled/interpreter.dSYM/Contents/Resources/Python/interpreter.py"

To run all discovered debug scripts in this session:

    settings set target.load-script-from-symbol-file true

Current executable set to '/Users/brucecollie/code/scratch/lesson-19-a-kompiled/interpreter' (x86_64).
(lldb) settings set -- target.run-args  ".krun-2023-03-20-11-22-46-TcYt9ffhb2/tmp.in.RupiLwHNfn" "-1" ".krun-2023-03-20-11-22-46-TcYt9ffhb2/result.kore"
(lldb) 
```

--------------------------------

### Define K Syntax and Rules for Color and Fruit

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/02_basics/README.md

This K definition introduces syntax for colors and fruits, and defines rules for the `colorOf` function. It demonstrates how to associate colors with specific fruits using pattern matching.

```k
module LESSON-02-D

  syntax Color ::= Yellow()
                 | Blue()
                 | Kiwi()
                 | colorOf(Fruit) [function]
  syntax Fruit ::= Banana()
                 | Blueberry()

  rule colorOf(Banana()) => Yellow()
  rule colorOf(Blueberry()) => Blue()

endmodule
```

--------------------------------

### Get Map Size (K)

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md

Returns the number of key/value pairs in a map. This operation has a time complexity of O(1). Uses the MAP.size hook and the sizeMap symbol.

```k
syntax Int ::= size(Map)                      [function, total, hook(MAP.size), symbol(sizeMap)]
```

--------------------------------

### General Maven Build Troubleshooting Commands

Source: https://github.com/runtimeverification/k/blob/master/README.md

Provides common Maven commands for troubleshooting build issues, including cleaning the project, updating snapshot dependencies, purging the local repository cache, and skipping tests during the build process.

```bash
mvn clean
mvn package -U
mvn dependency:purge-local-repository
mvn package -DskipTests
```

--------------------------------

### K Tutorial: LAMBDA++ Language Extensions

Source: https://github.com/runtimeverification/k/blob/master/web/toc.md

Details on extending the LAMBDA language to LAMBDA++ in K, including handling abrupt changes of control and semantic computation items.

```k
-- Example K definition for LAMBDA++ would go here.
```

--------------------------------

### K Rules for List Collection Operations

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

Illustrates K rules for introducing and eliminating elements from the start and end of a 'List' collection. These rules show how to manage list order and access elements from either end.

```k
rule <k> introduce-list-start(I:Int) => . ... </k>
     <lists> (.Bag => <list> I </list>) ... </lists>

rule <k> introduce-list-end(I:Int) => . ... </k>
     <lists> ... (.Bag => <list> I </list>) </lists>

rule <k> eliminate-list-start => I ... </k>
     <lists> (<list> I </list> => .Bag) ... </lists>

rule <k> eliminate-list-end => I ... </k>
     <lists> ... (<list> I </list> => .Bag) </lists>
```

--------------------------------

### K Module Definition and Imports

Source: https://github.com/runtimeverification/k/blob/master/pyk/regression-new/kprove-markdown/set-balance-spec.md

Defines the start of a K module named SET-BALANCE-SPEC and imports the VERIFICATION module. This is standard practice for structuring K specifications.

```k
module SET-BALANCE-SPEC
    imports VERIFICATION
```

--------------------------------

### Enable Nix Flakes Configuration

Source: https://github.com/runtimeverification/k/blob/master/README.md

This snippet shows how to enable experimental Nix features, specifically 'nix-command' and 'flakes', in the Nix configuration file. This is a prerequisite for using Nix flakes for building projects.

```nix
experimental-features = nix-command flakes
```

--------------------------------

### K Syntax and Semantic Lists for Function Call Stack

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/16_collections/README.md

Defines the syntax for expressions, statements, declarations, and programs using K, and imports necessary modules. It also sets up the initial configuration for an interpreter, including a function stack represented by a List.

```k
module LESSON-16-B-SYNTAX
  imports INT-SYNTAX
  imports ID-SYNTAX

  syntax Exp ::= Id "(" ")" | Int
  syntax Stmt ::= "return" Exp ";" [strict]
  syntax Decl ::= "fun" Id "(" ")" "{" Stmt "}"
  syntax Pgm ::= List{Decl,""}
  syntax Id ::= "main" [token]
endmodule

module LESSON-16-B
  imports LESSON-16-B-SYNTAX
  imports BOOL
  imports LIST

  configuration <T>
                  <k> $PGM:Pgm ~> main () </k>
                  <functions> .Map </functions>
                  <fstack> .List </fstack>
                </T>

  // declaration sequence
  rule <k> D:Decl P:Pgm => D ~> P ...</k>
  rule <k> .Pgm => . ...</k>

  // function definitions
  rule <k> fun X:Id () { S } => . ...</k>
       <functions>... .Map => X |-> S ...</functions>

  // function call
  syntax KItem ::= stackFrame(K)
  rule <k> X:Id () ~> K => S </k>
       <functions>... X |-> S ...</functions>
       <fstack> .List => ListItem(stackFrame(K)) ...</fstack>

  // return statement
  rule <k> return I:Int ; ~> _ => I ~> K </k>
       <fstack> ListItem(stackFrame(K)) => .List ...</fstack>

  syntax Bool ::= isKResult(K) [function, symbol]
  rule isKResult(_:Int) => true
  rule isKResult(_) => false [owise]
endmodule
```

--------------------------------

### K Simplification Lemma Example

Source: https://github.com/runtimeverification/k/blob/master/docs/user_manual.md

Shows a simplification lemma applied to a sizeWordStack function. This rule demonstrates the use of a 'requires' clause to prevent infinite cycles by ensuring the condition 'N =/=Int 0' is met.

```k
rule sizeWordStackAux(WS, N) => N +Int sizeWordStackAux(WS, 0)
  requires N =/=Int 0
  [simplification]
```

--------------------------------

### Kompiling K with Optimizations and Debug Info

Source: https://github.com/runtimeverification/k/blob/master/docs/ktools.md

Command to build the K project with optimizations and debug information enabled, using Maven.

```sh
mvn package -Dproject.build.type="FastBuild"
```

--------------------------------

### K Compilation and Parsing Commands

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/k-tutorial/1_basic/04_disambiguation/README.md

Commands to compile a K grammar definition and parse a program. The first example shows the default behavior leading to an ambiguity error, while the second uses a modified grammar to resolve it.

```bash
kompile lesson-04-e.k
kast --output kore dangling-else.if
```

```bash
kompile lesson-04-f.k
kast --output kast dangling-else.if
```

--------------------------------

### Get Bytes Length (K)

Source: https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md

Retrieves the length of a Bytes term in O(1) time. The result can be an Int or MInt. Currently, only 64-bit and 256-bit MInt types are supported.

```k
syntax Int ::= lengthBytes(Bytes) [function, total, hook(BYTES.length), smtlib(lengthBytes)]
  syntax {Width} MInt{Width} ::= lengthBytes(Bytes) [function, total, hook(BYTES.lengthMInt)]
```

--------------------------------

### K Configuration for Set-Balance Module

Source: https://github.com/runtimeverification/k/blob/master/pyk/regression-new/kprove-markdown/set-balance.md

Defines the initial state and configuration of the set-balance module. It includes components for actions, time, events, return values, call stack, fees, issuance, and a detailed account structure with balances and nonces. Dependencies include INT, DOMAINS, and COLLECTIONS modules.

```k
module SET-BALANCE
    imports INT
    imports DOMAINS
    imports COLLECTIONS

    configuration
      <set-balance>
        <k> $ACTION:Action </k>
        <now> 0 </now>
        <events> .List </events>
        <return-value> .Result </return-value>
        <call-stack> .List </call-stack>
        <existentialDeposit> 0 </existentialDeposit>
        <creationFee> 0 </creationFee>
        <transferFee> 0 </transferFee>
        <totalIssuance> 0 </totalIssuance>
        <accounts>
          <account multiplicity="*" type="Map">
            <accountID> .AccountId:AccountId </accountID>
            <freeBalance> 0 </freeBalance>
            <reservedBalance> 0 </reservedBalance>
            <vestingBalance> 0 </vestingBalance>
            <startingBlock> 0 </startingBlock>
            <perBlock> 0 </perBlock>
            <nonce> .Nonce </nonce>
            <locks> .Set </locks>
          </account>
        </accounts>
      </set-balance>

```