brick 2.10 → 2.13
raw patch · 11 files changed
Files
- CHANGELOG.md +37/−1
- README.md +4/−1
- brick.cabal +3/−3
- programs/AnimationDemo.hs +3/−3
- programs/ListDemo.hs +12/−0
- src/Brick/Types/Common.hs +2/−2
- src/Brick/Types/Internal.hs +46/−46
- src/Brick/Widgets/Core.hs +1/−1
- src/Brick/Widgets/FileBrowser.hs +34/−7
- src/Brick/Widgets/List.hs +48/−17
- tests/List.hs +14/−0
CHANGELOG.md view
@@ -2,6 +2,42 @@ Brick changelog --------------- +2.13+----++New features:++* Brick.Widgets.List: added support for wrapping (thanks Enrico Maria De+ Angelis). The List API now provides `setScrollWrap` to configure lists+ to wrap when moving their cursor, and the cursor-movement functions+ and event handlers now cause selection wrapping when a list has+ wrapping enabled. The `ListDemo` demo program was also updated to+ demonstrate the wrapping behavior.++2.12+----++Package changes:++* Raised upper bound on microlens to allow building with 0.5.++2.11+----++Bug fixes:++* Fixed a bug in FileBrowser: if a user pressed Enter when the cursor+ was on a selected entry, it was omitted from the list of+ selected browser entries. As part of this change, the function+ `actionFileBrowserSelectCurrent` previously toggled the selection+ of the entry at the cursor, but should have selected it instead.+ It now does so, and a new function for toggling was introduced:+ `actionFileBrowserToggleCurrent`.++Other changes:++* Upper bounds on `base` and `microlens` were adjusted.+ 2.10 ---- @@ -1848,7 +1884,7 @@ Bug fixes: * Fixed viewport behavior when the image in a viewport reduces its size enough to render the viewport offsets invalid. Before, this behavior- caused a crash during image croppin in vty; now the behavior is+ caused a crash during image cropping in vty; now the behavior is handled sanely (fixes #22; reported by Hans-Peter Deifel) 0.2.2
README.md view
@@ -105,13 +105,14 @@ | [`wrapping-editor`](https://github.com/ta0kira/wrapping-editor) | An embeddable editor with support for Brick | | [`youbrick`](https://github.com/florentc/youbrick) | A feed aggregator and launcher for Youtube channels | -These third-party packages also extend `brick`:+These additional packages also extend `brick`: | Project | Description | Hackage | | ------- | ----------- | ------- | | [`brick-filetree`](https://github.com/ChrisPenner/brick-filetree) | A widget for exploring a directory tree and selecting or flagging files and directories | [Hackage](https://hackage.haskell.org/package/brick-filetree) | | [`brick-panes`](https://github.com/kquick/brick-panes) | A Brick overlay library providing composition and isolation of screen areas for TUI apps. | [Hackage](https://hackage.haskell.org/package/brick-panes) | | [`brick-calendar`](https://github.com/ldgrp/brick-calendar) | A library providing a calendar widget for Brick-based applications. | [Hackage](https://hackage.haskell.org/package/brick-calendar) |+| [`brick-skylighting`](https://github.com/jtdaugherty/brick-skylighting) | A library providing integration support for [Skylighting](https://hackage.haskell.org/package/skylighting)-based syntax highlighting. | [Hackage](https://hackage.haskell.org/package/brick-skylighting) | Getting Started ---------------@@ -213,6 +214,8 @@ If you decide to contribute, that's great! Here are some guidelines you should consider to make submitting patches easier for all concerned: + - Patches written completely or partially by AI are unlikely to be+ accepted. Please disclose any AI use. - If you want to take on big things, talk to me first; let's have a design/vision discussion before you start coding. Create a GitHub issue and we can use that as the place to hash things out.
brick.cabal view
@@ -1,5 +1,5 @@ name: brick-version: 2.10+version: 2.13 synopsis: A declarative terminal user interface library description: Write terminal user interfaces (TUIs) painlessly with 'brick'! You@@ -108,7 +108,7 @@ Brick.Types.Internal Brick.Widgets.Internal - build-depends: base >= 4.9.0.0 && < 4.22.0.0,+ build-depends: base >= 4.9.0.0 && < 4.23.0.0, vty >= 6.0, vty-crossplatform, bimap >= 0.5 && < 0.6,@@ -117,7 +117,7 @@ exceptions >= 0.10.0, filepath, containers >= 0.5.7,- microlens >= 0.3.0.0,+ microlens >= 0.3.0.0 && < 0.6, microlens-th, microlens-mtl, mtl,
programs/AnimationDemo.hs view
@@ -94,9 +94,9 @@ [ withDefAttr attr6 $ str "0" , withDefAttr attr5 $ str "O" , withDefAttr attr4 $ str "o"- , withDefAttr attr3 $ str "*"- , withDefAttr attr2 $ str "~"- , withDefAttr attr1 $ str "."+ , withDefAttr attr3 $ str "•"+ , withDefAttr attr2 $ str "*"+ , withDefAttr attr2 $ str "." ] attr6 :: AttrName
programs/ListDemo.hs view
@@ -43,10 +43,16 @@ hLimit 25 $ vLimit 15 $ L.renderList listDrawElement True l+ wrapStatus = if L.getScrollWrap l+ then "enabled"+ else "disabled" ui = C.vCenter $ vBox [ C.hCenter box , str " " , C.hCenter $ str "Press +/- to add/remove list elements." , C.hCenter $ str "Press Esc to exit."+ , str " "+ , C.hCenter $ str "Press 'w' to toggle selection wrapping."+ , C.hCenter $ str $ "Selection wrapping is currently " <> wrapStatus <> "." ] appEvent :: T.BrickEvent () e -> T.EventM () (L.List () Char) ()@@ -64,6 +70,9 @@ Nothing -> return () Just i -> modify $ L.listRemove i + V.EvKey (V.KChar 'w') [] ->+ toggleListWrapping+ V.EvKey V.KEsc [] -> M.halt ev -> L.handleListEvent ev@@ -71,6 +80,9 @@ nextElement :: Vec.Vector Char -> Char nextElement v = fromMaybe '?' $ Vec.find (flip Vec.notElem v) (Vec.fromList ['a' .. 'z']) appEvent _ = return ()++toggleListWrapping :: T.EventM () (L.List () Char) ()+toggleListWrapping = L.listScrollWrapL %= not listDrawElement :: (Show a) => Bool -> a -> Widget () listDrawElement sel a =
src/Brick/Types/Common.hs view
@@ -24,7 +24,7 @@ #endif -- | A terminal screen location.-data Location = Location { loc :: (Int, Int)+data Location = Location { loc :: !(Int, Int) -- ^ (Column, Row) } deriving (Show, Eq, Ord, Read, Generic, NFData)@@ -48,7 +48,7 @@ mempty = origin mappend = (Sem.<>) -data Edges a = Edges { eTop, eBottom, eLeft, eRight :: a }+data Edges a = Edges { eTop, eBottom, eLeft, eRight :: !a } deriving (Eq, Ord, Read, Show, Functor, Generic, NFData) suffixLenses ''Edges
src/Brick/Types/Internal.hs view
@@ -103,16 +103,16 @@ import Brick.AttrMap (AttrName, AttrMap) import Brick.Widgets.Border.Style (BorderStyle) -data ScrollRequest = HScrollBy Int- | HScrollPage Direction+data ScrollRequest = HScrollBy !Int+ | HScrollPage !Direction | HScrollToBeginning | HScrollToEnd- | VScrollBy Int- | VScrollPage Direction+ | VScrollBy !Int+ | VScrollPage !Direction | VScrollToBeginning | VScrollToEnd- | SetTop Int- | SetLeft Int+ | SetTop !Int+ | SetLeft !Int deriving (Read, Show, Generic, NFData) -- | Widget size policies. These policies communicate how a widget uses@@ -131,9 +131,9 @@ -- | The type of widgets. data Widget n =- Widget { hSize :: Size+ Widget { hSize :: !Size -- ^ This widget's horizontal growth policy- , vSize :: Size+ , vSize :: !Size -- ^ This widget's vertical growth policy , render :: RenderM n (Result n) -- ^ This widget's rendering function@@ -230,21 +230,21 @@ } data VisibilityRequest =- VR { vrPosition :: Location- , vrSize :: DisplayRegion+ VR { vrPosition :: !Location+ , vrSize :: !DisplayRegion } deriving (Show, Eq, Read, Generic, NFData) -- | Describes the state of a viewport as it appears as its most recent -- rendering. data Viewport =- VP { _vpLeft :: Int+ VP { _vpLeft :: !Int -- ^ The column offset of left side of the viewport.- , _vpTop :: Int+ , _vpTop :: !Int -- ^ The row offset of the top of the viewport.- , _vpSize :: DisplayRegion+ , _vpSize :: !DisplayRegion -- ^ The size of the viewport.- , _vpContentSize :: DisplayRegion+ , _vpContentSize :: !DisplayRegion -- ^ The size of the contents of the viewport. } deriving (Show, Read, Generic, NFData)@@ -274,9 +274,9 @@ } data VtyContext =- VtyContext { vtyContextBuilder :: IO Vty- , vtyContextHandle :: Vty- , vtyContextThread :: ThreadId+ VtyContext { vtyContextBuilder :: !(IO Vty)+ , vtyContextHandle :: !Vty+ , vtyContextThread :: !ThreadId , vtyContextPutEvent :: Event -> IO () } @@ -330,27 +330,27 @@ -- | A border character has four segments, one extending in each direction -- (horizontally and vertically) from the center of the character. data BorderSegment = BorderSegment- { bsAccept :: Bool+ { bsAccept :: !Bool -- ^ Would this segment be willing to be drawn if a neighbor wanted to -- connect to it?- , bsOffer :: Bool+ , bsOffer :: !Bool -- ^ Does this segment want to connect to its neighbor?- , bsDraw :: Bool+ , bsDraw :: !Bool -- ^ Should this segment be represented visually? } deriving (Eq, Ord, Read, Show, Generic, NFData) -- | Information about how to redraw a dynamic border character when it abuts -- another dynamic border character. data DynBorder = DynBorder- { dbStyle :: BorderStyle+ { dbStyle :: !BorderStyle -- ^ The 'Char's to use when redrawing the border. Also used to filter -- connections: only dynamic borders with equal 'BorderStyle's will connect -- to each other.- , dbAttr :: Attr+ , dbAttr :: !Attr -- ^ What 'Attr' to use to redraw the border character. Also used to filter -- connections: only dynamic borders with equal 'Attr's will connect to -- each other.- , dbSegments :: Edges BorderSegment+ , dbSegments :: !(Edges BorderSegment) } deriving (Eq, Read, Show, Generic, NFData) -- | The type of result returned by a widget's rendering function. The@@ -394,23 +394,23 @@ } -- | The type of events.-data BrickEvent n e = VtyEvent Event+data BrickEvent n e = VtyEvent !Event -- ^ The event was a Vty event.- | AppEvent e+ | AppEvent !e -- ^ The event was an application event.- | MouseDown n Button [Modifier] Location+ | MouseDown !n !Button ![Modifier] !Location -- ^ A mouse-down event on the specified region was -- received. The 'n' value is the resource name of -- the clicked widget (see 'clickable').- | MouseUp n (Maybe Button) Location+ | MouseUp !n !(Maybe Button) !Location -- ^ A mouse-up event on the specified region was -- received. The 'n' value is the resource name of -- the clicked widget (see 'clickable'). deriving (Show, Eq, Ord) -data EventRO n = EventRO { eventViewportMap :: M.Map n Viewport- , latestExtents :: [Extent n]- , oldState :: RenderState n+data EventRO n = EventRO { eventViewportMap :: !(M.Map n Viewport)+ , latestExtents :: ![Extent n]+ , oldState :: !(RenderState n) } -- | Clickable elements of a scroll bar.@@ -432,22 +432,22 @@ -- to render, which bordering style should be used, and the attribute map -- available for rendering. data Context n =- Context { ctxAttrName :: AttrName- , availWidth :: Int- , availHeight :: Int- , windowWidth :: Int- , windowHeight :: Int- , ctxBorderStyle :: BorderStyle- , ctxAttrMap :: AttrMap- , ctxDynBorders :: Bool- , ctxVScrollBarOrientation :: Maybe VScrollBarOrientation- , ctxVScrollBarRenderer :: Maybe (VScrollbarRenderer n)- , ctxHScrollBarOrientation :: Maybe HScrollBarOrientation- , ctxHScrollBarRenderer :: Maybe (HScrollbarRenderer n)- , ctxVScrollBarShowHandles :: Bool- , ctxHScrollBarShowHandles :: Bool- , ctxVScrollBarClickableConstr :: Maybe (ClickableScrollbarElement -> n -> n)- , ctxHScrollBarClickableConstr :: Maybe (ClickableScrollbarElement -> n -> n)+ Context { ctxAttrName :: !AttrName+ , availWidth :: !Int+ , availHeight :: !Int+ , windowWidth :: !Int+ , windowHeight :: !Int+ , ctxBorderStyle :: !BorderStyle+ , ctxAttrMap :: !AttrMap+ , ctxDynBorders :: !Bool+ , ctxVScrollBarOrientation :: !(Maybe VScrollBarOrientation)+ , ctxVScrollBarRenderer :: !(Maybe (VScrollbarRenderer n))+ , ctxHScrollBarOrientation :: !(Maybe HScrollBarOrientation)+ , ctxHScrollBarRenderer :: !(Maybe (HScrollbarRenderer n))+ , ctxVScrollBarShowHandles :: !Bool+ , ctxHScrollBarShowHandles :: !Bool+ , ctxVScrollBarClickableConstr :: !(Maybe (ClickableScrollbarElement -> n -> n))+ , ctxHScrollBarClickableConstr :: !(Maybe (ClickableScrollbarElement -> n -> n)) } suffixLenses ''RenderState
src/Brick/Widgets/Core.hs view
@@ -340,7 +340,7 @@ -- input text should not contain escape sequences or carriage returns. txt :: T.Text -> Widget n txt s =- -- Althoguh vty Image uses lazy Text internally, using lazy text at this+ -- Although vty Image uses lazy Text internally, using lazy text at this -- level may not be an improvement. Indeed it can be much worse, due -- the overhead of lazy Text being significant compared to the typically -- short string content used to compose UIs.
src/Brick/Widgets/FileBrowser.hs view
@@ -71,6 +71,7 @@ , actionFileBrowserBeginSearch , actionFileBrowserSelectEnter , actionFileBrowserSelectCurrent+ , actionFileBrowserToggleCurrent , actionFileBrowserListPageUp , actionFileBrowserListPageDown , actionFileBrowserListHalfPageUp@@ -602,7 +603,7 @@ -- -- * @/@: 'actionFileBrowserBeginSearch' -- * @Enter@: 'actionFileBrowserSelectEnter'--- * @Space@: 'actionFileBrowserSelectCurrent'+-- * @Space@: 'actionFileBrowserToggleCurrent' -- * @g@: 'actionFileBrowserListTop' -- * @G@: 'actionFileBrowserListBottom' -- * @j@: 'actionFileBrowserListNext'@@ -625,6 +626,10 @@ actionFileBrowserSelectCurrent = selectCurrentEntry +actionFileBrowserToggleCurrent :: EventM n (FileBrowser n) ()+actionFileBrowserToggleCurrent =+ toggleCurrentEntrySelected+ actionFileBrowserListPageUp :: Ord n => EventM n (FileBrowser n) () actionFileBrowserListPageUp = zoom fileBrowserEntriesL listMovePageUp@@ -697,8 +702,8 @@ -- Select file or enter directory actionFileBrowserSelectEnter Vty.EvKey (Vty.KChar ' ') [] ->- -- Select entry- actionFileBrowserSelectCurrent+ -- Toggle selected status of current entry+ actionFileBrowserToggleCurrent _ -> handleFileBrowserEventCommon e @@ -730,12 +735,27 @@ toggleSelected :: FileInfo -> EventM n (FileBrowser n) () toggleSelected e = do+ sel <- fileBrowserIsSelected e+ if sel+ then fileBrowserRemoveSelected e+ else fileBrowserAddSelected e++fileBrowserIsSelected :: FileInfo -> EventM n (FileBrowser n) Bool+fileBrowserIsSelected e = do fs <- use fileBrowserSelectedFilesL let fName = fileInfoFilename e- if Set.member fName fs- then fileBrowserSelectedFilesL %= Set.delete fName- else fileBrowserSelectedFilesL %= Set.insert fName+ return $ Set.member fName fs +fileBrowserAddSelected :: FileInfo -> EventM n (FileBrowser n) ()+fileBrowserAddSelected e = do+ let fName = fileInfoFilename e+ fileBrowserSelectedFilesL %= Set.insert fName++fileBrowserRemoveSelected :: FileInfo -> EventM n (FileBrowser n) ()+fileBrowserRemoveSelected e = do+ let fName = fileInfoFilename e+ fileBrowserSelectedFilesL %= Set.delete fName+ -- | If the browser's current entry is selectable according to -- @fileBrowserSelectable@, add it to the selection set and return. -- If not, and if the entry is a directory or a symlink targeting a@@ -747,12 +767,19 @@ b <- get for_ (fileBrowserCursor b) $ \entry -> if fileBrowserSelectable b entry- then toggleSelected entry+ then fileBrowserAddSelected entry else when (selectDirectories entry) $ put =<< liftIO (setWorkingDirectory (fileInfoFilePath entry) b) selectCurrentEntry :: EventM n (FileBrowser n) () selectCurrentEntry = do+ b <- get+ for_ (fileBrowserCursor b) $ \entry ->+ when (fileBrowserSelectable b entry) $+ fileBrowserAddSelected entry++toggleCurrentEntrySelected :: EventM n (FileBrowser n) ()+toggleCurrentEntrySelected = do b <- get for_ (fileBrowserCursor b) $ \entry -> when (fileBrowserSelectable b entry) $
src/Brick/Widgets/List.hs view
@@ -22,6 +22,11 @@ -- * Constructing a list , list + -- * Configuring wrapping+ , setScrollWrap+ , getScrollWrap+ , listScrollWrapL+ -- * Rendering a list , renderList , renderListWithIndex@@ -103,8 +108,8 @@ import Brick.AttrMap -- | List state. Lists have a container @t@ of element type @e@ that is--- the data stored by the list. Internally, Lists handle the following--- events by default:+-- the data stored by the list. When using the event-handling functions+-- provided by this module, Lists handle the following events: -- -- * Up/down arrow keys: move cursor of selected item -- * Page up / page down keys: move cursor of selected item by one page@@ -112,6 +117,15 @@ -- * Home/end keys: move cursor of selected item to beginning or end of -- list --+-- Movement key behaviors (and their corresponding list transformation+-- functions) are subject to wrapping if the list's wrapping is enabled;+-- in that case, attempts to move the selection beyond either end of the+-- list will wrap the selection to the opposite end of the list. When+-- wrapping is disabled, attempts to move beyond either end of the list+-- will move the selection as far as possible without wrapping around+-- to the opposite end. To control whether wrapping is enabled, see+-- 'setScrollWrap'.+-- -- The 'List' type synonym fixes @t@ to 'V.Vector' for compatibility -- with previous versions of this library. --@@ -123,7 +137,6 @@ -- * 'listRemove': 'Semigroup' -- * 'listClear': 'Monoid' -- * 'listReverse': 'Reversible'--- data GenericList n t e = List { listElements :: !(t e) -- ^ The list's sequence of elements.@@ -133,6 +146,9 @@ -- ^ The list's name. , listItemHeight :: Int -- ^ The height of an individual item in the list.+ , listScrollWrap :: Bool+ -- ^ Whether moving beyond a list's first/last element+ -- should wrap to the last/first element. } deriving (Functor, Foldable, Traversable, Show, Generic) suffixLenses ''GenericList@@ -263,7 +279,8 @@ listSelectedFocusedAttr :: AttrName listSelectedFocusedAttr = listSelectedAttr <> attrName "focused" --- | Construct a list in terms of container 't' with element type 'e'.+-- | Construct a list, with wrapping initially disabled, in terms of+-- container 't' with element type 'e'. list :: (Foldable t) => n -- ^ The list name (must be unique)@@ -276,7 +293,7 @@ list name es h = let selIndex = if null es then Nothing else Just 0 safeHeight = max 1 h- in List es selIndex name safeHeight+ in List es selIndex name safeHeight False -- | Render a list using the specified item drawing function. --@@ -465,8 +482,8 @@ | otherwise = 0 in l' & listSelectedL .~ newSel --- | Move the list selected index up by one. (Moves the cursor up,--- subtracts one from the index.)+-- | Move the list selected index up by one (moves the cursor up,+-- subtracts one from the index), subject to wrapping. listMoveUp :: (Foldable t, Splittable t) => GenericList n t e -> GenericList n t e@@ -477,8 +494,8 @@ => EventM n (GenericList n t e) () listMovePageUp = listMoveByPages (-1::Double) --- | Move the list selected index down by one. (Moves the cursor down,--- adds one to the index.)+-- | Move the list selected index down by one (moves the cursor down,+-- adds one to the index), subject to wrapping. listMoveDown :: (Foldable t, Splittable t) => GenericList n t e -> GenericList n t e@@ -489,7 +506,8 @@ => EventM n (GenericList n t e) () listMovePageDown = listMoveByPages (1::Double) --- | Move the list selected index by some (fractional) number of pages.+-- | Move the list selected index by some (fractional) number of pages,+-- subject to wrapping. listMoveByPages :: (Foldable t, Splittable t, Ord n, RealFrac m) => m -> EventM n (GenericList n t e) ()@@ -506,8 +524,9 @@ -- | Move the list selected index. -- -- If the current selection is @Just x@, the selection is adjusted by--- the specified amount. The value is clamped to the extents of the list--- (i.e. the selection does not "wrap").+-- the specified amount. Whether the value is clamped to the extents of the+-- list or not (i.e. whether the selection doesn't wrap around the list or it+-- does), is determined by the list itself (see 'GenericList' for more info). -- -- If the current selection is @Nothing@ (i.e. there is no selection) -- and the direction is positive, set to @Just 0@ (first element),@@ -528,7 +547,10 @@ Nothing | amt > 0 -> 0 | otherwise -> length l - 1- Just i -> max 0 (amt + i) -- don't be negative+ Just i+ | let wrap = l ^. listScrollWrapL+ , wrap -> (amt + i) `mod` length l+ | otherwise -> max 0 (amt + i) -- don't be negative in listMoveTo target l -- | Set the selected index for a list to the specified index, subject@@ -623,7 +645,6 @@ -- O(n) -- set, modify, traverse -- listSelectedElementL for 'Seq.Seq': O(log(min(i, n - i))) -- all operations -- @--- listSelectedElementL :: (Splittable t, Traversable t, Semigroup (t e)) => Traversal' (GenericList n t e) e listSelectedElementL f l =@@ -674,8 +695,8 @@ l & listElementsL %~ reverse & listSelectedL %~ fmap (length l - 1 -) --- | Apply a function to the selected element. If no element is selected--- the list is not modified.+-- | Apply a function to the selected element. If no element is+-- selected, the list is not modified. -- -- Complexity: same as 'traverse' for the container type (typically -- /O(n)/).@@ -686,9 +707,19 @@ -- listModify for 'List': O(n) -- listModify for 'Seq.Seq': O(log(min(i, n - i))) -- @--- listModify :: (Traversable t, Splittable t, Semigroup (t e)) => (e -> e) -> GenericList n t e -> GenericList n t e listModify f = listSelectedElementL %~ f++-- | Sets the list's wrapping behavior; wrapping is enabled if given+-- @True@, or disabled if given @False@.+setScrollWrap :: (Traversable t, Splittable t, Semigroup (t e))+ => Bool -> GenericList n t e -> GenericList n t e+setScrollWrap b = listScrollWrapL .~ b++-- | Returns the list's wrapping setting; returns @True@ if wrapping is+-- enabled or @False@ otherwise.+getScrollWrap :: GenericList n t e -> Bool+getScrollWrap = listScrollWrap
tests/List.hs view
@@ -220,6 +220,20 @@ len = length l'' in maybe (len == 0) (== 0) (l'' ^. listSelectedL) +-- listMoveUp from beginning is the same as listMoveToEnd+prop_moveBeforeFirst :: Eq a => List n a -> Bool+prop_moveBeforeFirst l =+ let l' = setScrollWrap True l+ in listMoveUp (listMoveToBeginning l') =.= listMoveToEnd l'+ where (=.=) = (==) `on` (^. listSelectedL)++-- listMoveDown from end is the same as listMoveToBeginning+prop_moveAfterLast :: Eq a => List n a -> Bool+prop_moveAfterLast l =+ let l' = setScrollWrap True l+ in listMoveDown (listMoveToEnd l') =.= listMoveToBeginning l'+ where (=.=) = (==) `on` (^. listSelectedL)+ -- listMoveDown always reaches end of list (or list is empty) prop_moveDown :: (Eq a) => [ListOp a] -> List n a -> Bool prop_moveDown ops l =