diff options
| author | Alasdair Armstrong | 2017-07-12 13:05:22 +0100 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-07-12 13:05:22 +0100 |
| commit | 73c960dab16124dde513344777551b0bc4eacb88 (patch) | |
| tree | 16d672f0365dd3b016b9fc7bbc495b8b2344c1f8 /lib | |
| parent | 3bdd45856d908432e3b0d1af3f480c2311818a7c (diff) | |
Added vector range l-expressions and additional tests
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/prelude.sail | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/lib/prelude.sail b/lib/prelude.sail index b5ba261d..f3637945 100644 --- a/lib/prelude.sail +++ b/lib/prelude.sail @@ -161,15 +161,19 @@ val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure lteq_ val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gt_range_atom val forall Num 'n, Num 'm, Num 'o. ([|'n:'m|], [:'o:]) -> bool effect pure gteq_range_atom val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lt_atom_range -val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure lteq_atom_range val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gt_atom_range val forall Num 'n, Num 'm, Num 'o. ([:'n:], [|'m:'o|]) -> bool effect pure gteq_atom_range -overload (deinfix >=) [gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int] -overload (deinfix >) [gt_vec; gt_int] +val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lteq_atom_atom +val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gteq_atom_atom +val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure lt_atom_atom +val forall Num 'n, Num 'm. ([:'n:], [:'m:]) -> bool effect pure gt_atom_atom + +overload (deinfix >=) [gteq_atom_atom; gteq_range_atom; gteq_atom_range; gteq_vec; gteq_int] +overload (deinfix >) [gt_atom_atom; gt_vec; gt_int] overload (deinfix <=) [lteq_atom_atom; lteq_range_atom; lteq_atom_range; lteq_vec; lteq_int] -overload (deinfix <) [lt_vec; lt_int] +overload (deinfix <) [lt_atom_atom; lt_vec; lt_int] val (int, int) -> int effect pure quotient |