diff options
| author | Christopher Pulte | 2016-09-25 15:14:25 +0100 |
|---|---|---|
| committer | Christopher Pulte | 2016-09-25 15:14:25 +0100 |
| commit | 1cc29db33dd0f03d70314204f5d29a21a31857e4 (patch) | |
| tree | f54cd47521c61f7d0d9bc1419325af93af112e0a /language/l2.ott | |
| parent | dd052bfc3e00a1ae988044ae81dd1624332dd899 (diff) | |
| parent | d68d1e959091b186ebb5cbecf53992307b852f0d (diff) | |
Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail
Diffstat (limited to 'language/l2.ott')
| -rw-r--r-- | language/l2.ott | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/language/l2.ott b/language/l2.ott index 80bb5e26..84e92d7d 100644 --- a/language/l2.ott +++ b/language/l2.ott @@ -126,6 +126,7 @@ id :: '' ::= | reg :: M :: reg {{ ichlo (Id "reg") }} | to_num :: M :: tonum {{ com Built in function identifiers }} {{ ichlo (Id "to_num") }} | to_vec :: M :: tovec {{ ichlo (Id "to_vec") }} + | msb :: M :: msb {{ ichlo (Id "msb") }} % Note: we have just a single namespace. We don't want the same % identifier to be reused as a type name or variable, expression % variable, and field name. We don't enforce any lexical convention @@ -986,6 +987,8 @@ terminals :: '' ::= {{ tex \ensuremath{\vdash_e} }} | |-o :: :: vdashO {{ tex \ensuremath{\vdash_o} }} + | |-c :: :: vdashC + {{ tex \ensuremath{\vdash_c} }} | ' :: :: quote {{ tex \mbox{'} }} | |-> :: :: mapsto |