diff options
Diffstat (limited to 'language/primitive_doc.ott')
| -rw-r--r-- | language/primitive_doc.ott | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/language/primitive_doc.ott b/language/primitive_doc.ott index 2a0c2c0f..e96f6065 100644 --- a/language/primitive_doc.ott +++ b/language/primitive_doc.ott @@ -95,8 +95,16 @@ functions :: '' ::= {{ com bitwise and }} | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : & :: :: andvec | val ( bit , bit ) -> bit : ^ :: :: xor - {{ com bitwise xor ^ will fix gen later }} + {{ com bitwise xor }} | val forall Nat 'n . ( bit [ 'n ] , bit [ 'n ] ) -> bit [ 'n ] : '^' :: :: xorvec + | val forall Nat 'n . ( bit , [| 'n |] ) -> bit [ 'n ] : '^^' :: :: duplicate + {{ com duplicate bit into a vector }} + | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : << :: :: lshift + {{ com left shift }} + | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : >> :: :: rshift + {{ com right shift }} + | val forall Nat 'n , Nat 'm , 'm <= 'n . ( bit [ 'n ] , [| 'm |] ) -> bit [ 'n ] : <<< :: :: rotate + {{ com rotate }} functions_with_coercions :: '' ::= |