Skip to content

Commit

Permalink
inline: always
Browse files Browse the repository at this point in the history
  • Loading branch information
lukaszcz committed Oct 12, 2023
1 parent 8493ff4 commit 6a76d4f
Showing 1 changed file with 2 additions and 0 deletions.
2 changes: 2 additions & 0 deletions Stdlib/Data/Range.juvix
Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,13 @@ for {A N} {{Ord N}} {{Natural N}} (f : A → N → A) (a : A)
syntax operator to range;

--- `x to y` is the range [x..y]
{-# inline: always #-}
to {N} {{Natural N}} (l h : N) : Range N :=
mkRange l h (fromNat 1);

syntax operator step step;

--- `x to y step s` is the range [x,x+s,..,y]
{-# inline: always #-}
step {N} (r : Range N) (s : N) : Range N :=
r@Range{step := s};

0 comments on commit 6a76d4f

Please sign in to comment.