diff options
Diffstat (limited to 'cheri')
| -rw-r--r-- | cheri/cheri_prelude_128.sail | 4 | ||||
| -rw-r--r-- | cheri/cheri_prelude_256.sail | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/cheri/cheri_prelude_128.sail b/cheri/cheri_prelude_128.sail index f1f33a56..5e63221e 100644 --- a/cheri/cheri_prelude_128.sail +++ b/cheri/cheri_prelude_128.sail @@ -35,8 +35,8 @@ (* 128 bit cap + tag *) typedef CapReg = bit[129] -val cast bool -> bit effect pure cast_bool_bit -val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec +val cast extern bool -> bit effect pure cast_bool_bit +val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) val extern bool -> bool effect pure not diff --git a/cheri/cheri_prelude_256.sail b/cheri/cheri_prelude_256.sail index 7cf3d69c..7b42020d 100644 --- a/cheri/cheri_prelude_256.sail +++ b/cheri/cheri_prelude_256.sail @@ -35,8 +35,8 @@ (* 256 bit cap + tag *) typedef CapReg = bit[257] -val cast bool -> bit effect pure cast_bool_bit -val cast forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec +val cast extern bool -> bit effect pure cast_bool_bit +val cast extern forall 'n, 'm. vector<'n,'m,dec,bool> -> vector<'n,'m,dec,bit> effect pure cast_boolvec_bitvec val cast forall 'm. [|0:2**'m - 1|] -> vector<'m - 1,'m,dec,bit> effect pure cast_range_bitvec function vector<'m - 1,'m,dec,bit> cast_range_bitvec (v) = to_vec (v) val extern bool -> bool effect pure not |