Use 'Prop' instead of '@' to write the kind of a constraint.

This is more consistent with how we've been printing kinds for a while,
so no need to change the notation.

lib/Cryptol.cry

@@ -48,34 +48,34 @@ primitive type Z : # -> *
 
 
 /** Assert that two numeric types are equal. */
-primitive type (==) : # -> # -> @
+primitive type (==) : # -> # -> Prop
 
 /** Assert that two numeric types are different. */
-primitive type (!=) : # -> # -> @
+primitive type (!=) : # -> # -> Prop
 
 /** Assert that the first numeric type is larger than, or equal to the second.*/
-primitive type (>=) : # -> # -> @
+primitive type (>=) : # -> # -> Prop
 
 /** Assert that a numeric type is a proper natural number (not 'inf'). */
-primitive type fin : * -> @
+primitive type fin : * -> Prop
 
 /** Value types that have a notion of 'zero'. */
-primitive type Zero : * -> @
+primitive type Zero : * -> Prop
 
 /** Value types that support logical operations. */
-primitive type Logic : * -> @
+primitive type Logic : * -> Prop
 
 /** Value types that support arithmetic. */
-primitive type Arith : * -> @
+primitive type Arith : * -> Prop
 
 /** Value types that support unsigned comparisons. */
-primitive type Cmp : * -> @
+primitive type Cmp : * -> Prop
 
 /** Value types that support signed comparisons. */
-primitive type SignedCmp : * -> @
+primitive type SignedCmp : * -> Prop
 
 /** 'Literal n a' asserts that type 'a' contains the number 'n'. */
-primitive type Literal : # -> * -> @
+primitive type Literal : # -> * -> Prop
 
 
 

src/Cryptol/Parser.y

@@ -81,6 +81,7 @@ import Paths_cryptol
 
   'primitive' { Located $$ (Token (KW KW_primitive) _)}
   'constraint'{ Located $$ (Token (KW KW_constraint) _)}
+  'Prop'      { Located $$ (Token (KW KW_Prop) _)}
 
   '['         { Located $$ (Token (Sym BracketL) _)}
   ']'         { Located $$ (Token (Sym BracketR) _)}
@@ -633,11 +634,11 @@ schema_quals                   :: { Located [Prop PName] }
 schema_qual                    :: { Located [Prop PName] }
   : type '=>'                     {% fmap (\x -> at (x,$2) x) (mkProp $1) }
 
-kind                             :: { Located Kind      }
-  : '#'                             { Located $1 KNum   }
-  | '*'                             { Located $1 KType  }
-  | '@'                             { Located $1 KProp  }
-  | kind '->' kind                  { combLoc KFun $1 $3 }
+kind                           :: { Located Kind      }
+  : '#'                           { Located $1 KNum   }
+  | '*'                           { Located $1 KType  }
+  | 'Prop'                        { Located $1 KProp  }
+  | kind '->' kind                { combLoc KFun $1 $3 }
 
 schema_param                   :: { TParam PName }
   : ident                         {% mkTParam $1 Nothing           }

src/Cryptol/Parser/Lexer.x

@@ -121,6 +121,8 @@ $white+                   { emit $ White Space }
 "parameter"               { emit $ KW KW_parameter }
 "constraint"              { emit $ KW KW_constraint }
 
+"Prop"                    { emit $ KW KW_Prop }
+
 @num2                     { emitS (numToken 2  . Text.drop 2) }
 @num8                     { emitS (numToken 8  . Text.drop 2) }
 @num10                    { emitS (numToken 10 . Text.drop 0) }

src/Cryptol/Parser/LexerUtils.hs

@@ -393,6 +393,7 @@ data TokenKW  = KW_else
               | KW_primitive
               | KW_parameter
               | KW_constraint
+              | KW_Prop
                 deriving (Eq, Show, Generic, NFData)
 
 -- | The named operators are a special case for parsing types, and 'Other' is

src/Cryptol/Prelude.hs

@@ -18,7 +18,6 @@ module Cryptol.Prelude (
   cryptolTcContents
   ) where
 
-
 import System.Directory (getTemporaryDirectory)
 import System.IO (hClose, hPutStr, openTempFile)
 import Text.Heredoc (there)