Skip to content

Commit c42b8f0

Browse files
authored
Adjust name for =/=K hook (#3835)
The name used in the Haskell backend was `KEQUAL.neq` but [the K `domains.md` file uses `KEQUAL.ne`](https://github.com/runtimeverification/k/blob/master/k-distribution/include/kframework/builtin/domains.md?plain=1#L2287).
1 parent 7735c2f commit c42b8f0

File tree

4 files changed

+7
-7
lines changed

4 files changed

+7
-7
lines changed

docs/hooks.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -836,13 +836,13 @@ Comparison: is the first argument equal to the second?
836836
~~~
837837

838838

839-
### KEQUAL.neq
839+
### KEQUAL.ne
840840

841841
Comparison: is the first argument inequal to the second?
842842

843843
~~~
844844
hooked-symbol neq{}(Item{}, Item{}) : Bool{}
845-
[hook{}("KEQUAL.neq")]
845+
[hook{}("KEQUAL.ne")]
846846
~~~
847847

848848
### KEQUAL.ite

docs/manual/DEVELOPER_MANUAL.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -100,7 +100,7 @@
100100
8. [SET.list2set](#implementation-hooks-set-list2set)
101101
7. [KEQUAL](#implementation-hooks-kequal)
102102
1. [KEQUAL.eq](#implementation-hooks-kequal-eq)
103-
2. [KEQUAL.neq](#implementation-hooks-kequal-neq)
103+
2. [KEQUAL.ne](#implementation-hooks-kequal-neq)
104104
3. [KEQUAL.ite](#implementation-hooks-kequal-ite)
105105
8. [KRYPTO](#implementation-hooks-krypto)
106106
1. [KRYPTO.keccak256](#implementation-hooks-krypto-keccak266)

kore/src/Kore/Builtin/KEqual.hs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -122,10 +122,10 @@ symbolVerifiers =
122122
++ " in KEQUAL.ite"
123123
)
124124

125-
{- | @builtinFunctions@ defines the hooks for @KEQUAL.eq@, @KEQUAL.neq@, and
125+
{- | @builtinFunctions@ defines the hooks for @KEQUAL.eq@, @KEQUAL.ne@, and
126126
@KEQUAL.ite@.
127127
128-
@KEQUAL.eq@ and @KEQUAL.neq@ can take arbitrary terms (of the same sort) and
128+
@KEQUAL.eq@ and @KEQUAL.ne@ can take arbitrary terms (of the same sort) and
129129
check whether they are equal or not, producing a builtin boolean value.
130130
131131
@KEQUAL.ite@ can take a boolean expression and two arbitrary terms (of the same
@@ -198,7 +198,7 @@ eqKey :: IsString s => s
198198
eqKey = "KEQUAL.eq"
199199

200200
neqKey :: IsString s => s
201-
neqKey = "KEQUAL.neq"
201+
neqKey = "KEQUAL.ne"
202202

203203
iteKey :: IsString s => s
204204
iteKey = "KEQUAL.ite"

kore/test/Test/Kore/Builtin/Definition.hs

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -316,7 +316,7 @@ comparisonKSymbol name = comparisonSymbol name kSort
316316
keqBoolSymbol :: Internal.Symbol
317317
keqBoolSymbol = comparisonKSymbol "keqBool" & hook "KEQUAL.eq"
318318
kneqBoolSymbol :: Internal.Symbol
319-
kneqBoolSymbol = comparisonKSymbol "kneqBool" & hook "KEQUAL.neq"
319+
kneqBoolSymbol = comparisonKSymbol "kneqBool" & hook "KEQUAL.ne"
320320
kiteKSymbol :: Internal.Symbol
321321
kiteKSymbol =
322322
builtinSymbol "kiteK" kSort [boolSort, kSort, kSort]

0 commit comments

Comments
 (0)