diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index 6eb21f05..698a39a0 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -12,7 +12,7 @@ val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'l >= 0, 'm <= 'o, 'o <= 'l. (vector<'n,'l,inc,'a>, [:'m:], [:'o:]) -> vector<'m,'o - 'm,inc,'a> effect pure vector_subrange_inc val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. - (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange_dec + (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,('m - 'o) - 1,dec,'a> effect pure vector_subrange_dec overload vector_subrange [vector_subrange_inc; vector_subrange_dec] @@ -141,7 +141,7 @@ val (bool, bool) -> bool effect pure bool_and overload ~ [bool_not] overload (deinfix &) [bool_and] -overload (deinfix | ) [bool_or] +overload (deinfix |) [bool_or] (* val forall Nat 'n, Nat 'l, Nat 'm, Nat 'o, Type 'a, 'n >= 'm, 'm >= 'o, 'o >= 'n - 'l + 1. (vector<'n,'l,dec,'a>, [:'m:], [:'o:]) -> vector<'m,'m - 'o - 1,dec,'a> effect pure vector_subrange |