From 494fdfdf17950cd5e8f80e9ce47866e4415de3c6 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 18 Mar 2026 14:23:45 +0100 Subject: [PATCH 01/10] s/expoennt/exponent --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 23de7240d3f..6f4c88af0f1 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1471,7 +1471,7 @@ The syntax of ordinary floating-point values in K consists of an optional sign followed by an optional fractional part. Either the integer part or the fractional part must be specified. The mantissa is followed by an optional exponent part, which consists of an `e` or `E`, an optional sign (+ or -), -and an integer. The expoennt is followed by an optional suffix, which can be +and an integer. The exponent is followed by an optional suffix, which can be either `f`, `F`, `d`, `D`, or `pNxM` where `N` and `M` are positive integers. `p` and `x` can be either upper or lowercase. diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index fa610218faf..6c90af8ecba 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -1449,7 +1449,7 @@ The syntax of ordinary floating-point values in K consists of an optional sign followed by an optional fractional part. Either the integer part or the fractional part must be specified. The mantissa is followed by an optional exponent part, which consists of an `e` or `E`, an optional sign (+ or -), -and an integer. The expoennt is followed by an optional suffix, which can be +and an integer. The exponent is followed by an optional suffix, which can be either `f`, `F`, `d`, `D`, or `pNxM` where `N` and `M` are positive integers. `p` and `x` can be either upper or lowercase. From e61d5ea4658d4133169e026b322de51134bb5bc2 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 20 Mar 2026 17:46:26 +0100 Subject: [PATCH 02/10] s/equasl/equals --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 6f4c88af0f1..3e344d3b171 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1628,7 +1628,7 @@ You can: ### Floating-point comparisons -Compute whether a float is less than or equasl to, less than, greater than or +Compute whether a float is less than or equals to, less than, greater than or equal to, greater than, equal, or unequal to another float. Note that `X ==Float Y` and `X ==K Y` might yield different values. The latter should be used in cases where you want to compare whether two values of sort `Float` diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index 6c90af8ecba..83290272e4d 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -1606,7 +1606,7 @@ You can: ### Floating-point comparisons -Compute whether a float is less than or equasl to, less than, greater than or +Compute whether a float is less than or equals to, less than, greater than or equal to, greater than, equal, or unequal to another float. Note that `X ==Float Y` and `X ==K Y` might yield different values. The latter should be used in cases where you want to compare whether two values of sort `Float` From b756da1fe65356d5d4f2b854880e6cfec1c70079 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:14:00 +0200 Subject: [PATCH 03/10] s/mached/matched --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 3e344d3b171..d5c193de0d0 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -714,7 +714,7 @@ side and all variables are bound, it is O(N*log(M)) where M is the size of the set it is matching and N is the number of elements being matched. When it appears on the left hand side containing variables not bound elsewhere in the term, it is O(N^K) where N is the size of the set it is matching and K is the -number of unbound keys being mached. In other words, one unbound variable is +number of unbound keys being matched. In other words, one unbound variable is linear, two is quadratic, three is cubic, etc. ```k diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index 83290272e4d..8d1893958e9 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -714,7 +714,7 @@ side and all variables are bound, it is O(N*log(M)) where M is the size of the set it is matching and N is the number of elements being matched. When it appears on the left hand side containing variables not bound elsewhere in the term, it is O(N^K) where N is the size of the set it is matching and K is the -number of unbound keys being mached. In other words, one unbound variable is +number of unbound keys being matched. In other words, one unbound variable is linear, two is quadratic, three is cubic, etc. ```k From e98ae818f866c3114eaa24a9de084e00efa205f5 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:14:59 +0200 Subject: [PATCH 04/10] s/constucted/constructed --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index d5c193de0d0..05901b35e5d 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -940,7 +940,7 @@ The list with zero elements is represented by `.List`. ### List elements -An element of a `List` is constucted via the `ListItem` operator. +An element of a `List` is constructed via the `ListItem` operator. ```k syntax List ::= ListItem(KItem) [function, total, hook(LIST.element), symbol(ListItem), smtlib(smt_seq_elem)] diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index 8d1893958e9..d5e402812c2 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -939,7 +939,7 @@ The list with zero elements is represented by `.List`. ### List elements -An element of a `List` is constucted via the `ListItem` operator. +An element of a `List` is constructed via the `ListItem` operator. ```k syntax List ::= ListItem(KItem) [function, total, hook(LIST.element), klabel(ListItem), symbol, smtlib(smt_seq_elem)] From 05261edb60fc09bdb01492839b57915cf01669ad Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:16:03 +0200 Subject: [PATCH 05/10] s/indice/index --- k-distribution/include/kframework/builtin/domains.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 05901b35e5d..8ca9cb30ff4 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -960,7 +960,7 @@ An element can be added to the front of a `List` using the `pushList` operator. You can get an element of a list by its integer offset in O(log(N)) time, or effectively constant. Positive `Int` indices are 0-indexed from the beginning of the list, and negative indices are -1-indexed from the end of the list. In other -words, 0 is the first element and -1 is the last element. The indice can also be +words, 0 is the first element and -1 is the last element. The index can also be `MInt`, which is interprested as an unsigned integer, and therefore, don't support negative indices feature. Currently, only 64-bit and 256-bit `MInt` types are supported. From b4f09c6036ea69fad3fef40886950a4db22e29a5 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:16:55 +0200 Subject: [PATCH 06/10] add whitespace --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 8ca9cb30ff4..2ec64fee7c1 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -992,7 +992,7 @@ time. You can create a new `List` which is equal to `dest` except the `N` elements starting at `index` are replaced with the contents of `src` in O(N*log(K)) time -(where `K` is the size of `dest`and `N` is the size of `src`), or effectively linear. Having `index + N > K` yields an exception. +(where `K` is the size of `dest` and `N` is the size of `src`), or effectively linear. Having `index + N > K` yields an exception. ```k syntax List ::= updateList(dest: List, index: Int, src: List) [function, hook(LIST.updateAll)] diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index d5e402812c2..1ff00b51308 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -978,7 +978,7 @@ time. You can create a new `List` which is equal to `dest` except the `N` elements starting at `index` are replaced with the contents of `src` in O(N*log(K)) time -(where `K` is the size of `dest`and `N` is the size of `src`), or effectively linear. Having `index + N > K` yields an exception. +(where `K` is the size of `dest` and `N` is the size of `src`), or effectively linear. Having `index + N > K` yields an exception. ```k syntax List ::= updateList(dest: List, index: Int, src: List) [function, hook(LIST.updateAll)] From e37f4022b62710ffb71a8c4d08dc0f9268215c95 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:18:32 +0200 Subject: [PATCH 07/10] s/interpeted/interpreted --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 2ec64fee7c1..93f8ece2f4a 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1307,7 +1307,7 @@ is `#False`. ### Bit slicing You can compute the value of a range of bits in the twos-complement -representation of an integer, as interpeted either unsigned or signed, of an +representation of an integer, as interpreted either unsigned or signed, of an integer. `index` is offset from 0 and `length` is the number of bits, starting with `index`, that should be read. The number is assumed to be represented in little endian notation with each byte going from least significant to diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index 1ff00b51308..f4f542be9c6 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -1283,7 +1283,7 @@ is `#False`. ### Bit slicing You can compute the value of a range of bits in the twos-complement -representation of an integer, as interpeted either unsigned or signed, of an +representation of an integer, as interpreted either unsigned or signed, of an integer. `index` is offset from 0 and `length` is the number of bits, starting with `index`, that should be read. The number is assumed to be represented in little endian notation with each byte going from least significant to From 34a11d1378f29af01e2f4841304bc1d6d34aeaf5 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:20:53 +0200 Subject: [PATCH 08/10] s/rigth/right --- k-distribution/include/kframework/builtin/domains.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 93f8ece2f4a..7b86eb8296e 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1403,9 +1403,9 @@ module INT-KORE [symbolic] rule [eq-k-to-eq-int] : I1:Int ==K I2:Int => I1 ==Int I2 [simplification] rule [eq-int-true-left] : {K1 ==Int K2 #Equals true} => {K1 #Equals K2} [simplification] - rule [eq-int-true-rigth] : {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification] + rule [eq-int-true-right] : {true #Equals K1 ==Int K2} => {K1 #Equals K2} [simplification] rule [eq-int-false-left] : {K1 ==Int K2 #Equals false} => #Not({K1 #Equals K2}) [simplification] - rule [eq-int-false-rigth] : {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification] + rule [eq-int-false-right] : {false #Equals K1 ==Int K2} => #Not({K1 #Equals K2}) [simplification] rule [neq-int-true-left] : {K1 =/=Int K2 #Equals true} => #Not({K1 #Equals K2}) [simplification] rule [neq-int-true-right] : {true #Equals K1 =/=Int K2} => #Not({K1 #Equals K2}) [simplification] rule [neq-int-false-left] : {K1 =/=Int K2 #Equals false} => {K1 #Equals K2} [simplification] From eac54c288ffb2b160423bd78d2be62e1dd2f303c Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:21:43 +0200 Subject: [PATCH 09/10] add capitalisation (F) --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index 7b86eb8296e..cebacc42178 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1481,7 +1481,7 @@ power of the exponent, which is interpreted as an integer, and defaults to zero if it is not present. Finally, it is rounded to the nearest possible value in a floating-point type represented like an IEEE754 floating-point type, with the number of bits of precision and exponent specified by the suffix. -A suffix of `f` or `f` represents the IEEE `binary32` format. A suffix of `d` +A suffix of `f` or `F` represents the IEEE `binary32` format. A suffix of `d` or `D`, or no suffix, represents the IEEE `binary64` format. A suffix of `pNxM` (either upper or lowercase) specifies exactly `N` bits of precision and `M` bits of exponent. The number of bits of precision is assumed to include diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index f4f542be9c6..4fd9a07a9ff 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -1459,7 +1459,7 @@ power of the exponent, which is interpreted as an integer, and defaults to zero if it is not present. Finally, it is rounded to the nearest possible value in a floating-point type represented like an IEEE754 floating-point type, with the number of bits of precision and exponent specified by the suffix. -A suffix of `f` or `f` represents the IEEE `binary32` format. A suffix of `d` +A suffix of `f` or `F` represents the IEEE `binary32` format. A suffix of `d` or `D`, or no suffix, represents the IEEE `binary64` format. A suffix of `pNxM` (either upper or lowercase) specifies exactly `N` bits of precision and `M` bits of exponent. The number of bits of precision is assumed to include From 3c7d2ddc55f10cb34198c94b807cd9595d1c923d Mon Sep 17 00:00:00 2001 From: dkcumming Date: Thu, 30 Apr 2026 13:23:18 +0200 Subject: [PATCH 10/10] s/tanFlooat/tanFloat --- k-distribution/include/kframework/builtin/domains.md | 2 +- pyk/src/tests/profiling/test-data/domains.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/k-distribution/include/kframework/builtin/domains.md b/k-distribution/include/kframework/builtin/domains.md index cebacc42178..69f8a050f37 100644 --- a/k-distribution/include/kframework/builtin/domains.md +++ b/k-distribution/include/kframework/builtin/domains.md @@ -1590,7 +1590,7 @@ You can: * Compute the natural logarithm `logFloat` of a float. * Compute the sine `sinFloat` of a float. * Compute the cosine `cosFloat` of a float. -* Compute the tangent `tanFlooat` of a float. +* Compute the tangent `tanFloat` of a float. * Compute the arcsine `asinFloat` of a float. * Compute the arccosine `acosFloat` of a float. * Compute the arctangent `atanFloat` of a float. diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md index 4fd9a07a9ff..6506ee25938 100644 --- a/pyk/src/tests/profiling/test-data/domains.md +++ b/pyk/src/tests/profiling/test-data/domains.md @@ -1568,7 +1568,7 @@ You can: * Compute the natural logarithm `logFloat` of a float. * Compute the sine `sinFloat` of a float. * Compute the cosine `cosFloat` of a float. -* Compute the tangent `tanFlooat` of a float. +* Compute the tangent `tanFloat` of a float. * Compute the arcsine `asinFloat` of a float. * Compute the arccosine `acosFloat` of a float. * Compute the arctangent `atanFloat` of a float.