From 24b138ee245ea23f8b7b97fdaa223a7fabdf7850 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 18 Mar 2026 14:23:45 +0100 Subject: [PATCH 1/2] 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 aa3bc18b8936a594c3fdd68e33a95a0eeba36982 Mon Sep 17 00:00:00 2001 From: dkcumming Date: Fri, 20 Mar 2026 17:46:26 +0100 Subject: [PATCH 2/2] 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`