= is the "mathematical" equality, which reduces to theorem proving, while == is the structural one.  Andrei, can you please send a pertinent paragraph explaining the difference between them, so Kevin can incorporate it in the documentation?

Grigore


________________________________
From: traiansf [notifications@github.com]
Sent: Tuesday, March 04, 2014 3:03 AM
To: kframework/k
Subject: Re: [k] Added many documentation comments; added a "nodoc" tag. (#264)


In include/builtins/int.k:

> @@ -52,6 +59,11 @@ module INT-HOOKS
>    // rule absInt(I:Int) => I when I >=Int 0
>    // rule absInt(I:Int) => 0 -Int I when I <Int 0
>
> +  /*@ The following is a list of boolean operators on Integers. These follow C-style conventions
> +   Except for  ``is not equal to", which is ``=\=Int" instead of ``!=Int".
> +   ``=Int" is equivalent to ``==Int"; both check for equality.
> +   ``dividesInt" performs modulus and checks to see if the result is 0.*/


There are some distinctions between =Int and ==Int, but I don't feel the most qualified to talk about them. Andrei, Grigore?

—
Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/264/files#r10247055>.