diff options
| author | Alasdair Armstrong | 2017-06-29 20:02:03 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-06-29 20:02:03 +0100 |
| commit | 6ca1722c9f804d79704fcc8681c9765b6040445b (patch) | |
| tree | 45e1524d0e9b154f6f4a881c41311637e0adec6f /lib | |
| parent | 4c712104db3a178fd8316a2bb36f2f241f249d2d (diff) | |
Added a large test case to the test-suite
Commented out some buggy re-sugaring logic from pretty_print_common
where it re-sugared vectors incorrectly
Fixed a bug where the type checker forgot to preserve type signatures
in top-level letbinds
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 |