Document signatures of implicit Kore definitions (#1949)

* Remove "The Semantics of K"

"The Semantics of K" document is obsolete and should not serve as a reference to
the current state of Kore.

* docs/kore-syntax.md: Correct syntax of fixpoints

* docs/kore-implicits.md

Author: ttuegel

docs/kore-implicits.md

@@ -0,0 +1,63 @@
+# Sorts of Kore implicits
+
+This document describes the sort signatures of the Kore implicits.
+
+## Connectives
+
+```
+\top{S}() : S
+\bottom{S}() : S
+```
+
+```
+\not{S}(S) : S
+```
+
+```
+\and{S}(S, S) : S
+\or{S}(S, S) : S
+\implies{S}(S, S) : S
+\iff{S}(S, S) : S
+```
+
+## Quantifiers
+
+```
+\exists{S}(x:T, S)
+\forall{S}(x:T, S)
+```
+
+## Fixpoints
+
+```
+\mu{}(@X:S, S) : S
+\nu{}(@X:S, S) : S
+```
+
+## Predicates
+
+```
+\ceil{S, R}(S) : R
+\floor{S, R}(S) : R
+```
+
+```
+\equals{S, R}(S, S) : R
+\in{S, R}(S, S) : R
+```
+
+## Rewriting
+
+```
+\next{S}(S) : S
+```
+
+```
+\rewrites{S}(S, S) : S
+```
+
+## Domain values
+
+```
+\dv{S}(#String) : S
+```

docs/kore-syntax.md

@@ -139,9 +139,9 @@ properly defined at the end of this section.
     | "\forall" "{" <sort> "}"
         "(" <element-variable> "," <pattern> ")"
     // Fixpoint operators
-    | "\mu" "{" <sort> "}"
+    | "\mu" "{" "}"
         "(" <set-variable> "," <pattern> ")"
-    | "\nu" "{" <sort> "}"
+    | "\nu" "{" "}"
         "(" <set-variable> "," <pattern> ")"
     // Definedness and totality
     | "\ceil" "{" <sort> "," <sort> "}"
@@ -297,4 +297,3 @@ Keywords
 ```
 
 An identifier cannot be a keyword.
-