diff options
| author | Thomas Bauereiss | 2017-07-12 13:10:53 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2017-07-12 13:10:53 +0100 |
| commit | b6b0dad963e640a5fd2b3ad2eabd0738b46b4c9c (patch) | |
| tree | 7171cd64a08b9a3bd9a80524947be31946e326e8 /lib | |
| parent | 4ba73e1e36a8ebda34d8d3afa6dbeff6256d262a (diff) | |
| parent | 73c960dab16124dde513344777551b0bc4eacb88 (diff) | |
Merge
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 |