a596776 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Remove deprecated calls to return

commita59677632a47b727f3682ee8d3250d2c48c58b99 authorMarkus Klink <markus.klink@inoio.de> dateThu 29 Sep 2016, 11:39 (10 years ago) parent8ea8a38

2 files changed+3−3

unifiedsplit

samples/effects/TreeTag.idr+2−2

@@ -20,13 +20,13 @@ testTree = Node (Node Leaf "Jim" Leaf)

2020 (Node Leaf "Bob" Leaf))

2121

2222treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))

23−treeTagAux Leaf = return Leaf

23+treeTagAux Leaf = pure Leaf

2424treeTagAux (Node l x r)

2525 = do l' <- treeTagAux l

2626 i <- get

2727 put (i + 1)

2828 r' <- treeTagAux r

29− return (Node l' (i, x) r')

29+ pure (Node l' (i, x) r')

3030

3131treeTag : (i : Int) -> BTree a -> BTree (Int, a)

3232treeTag i x = runPure (do put i

samples/tutorial/classes.idr+1−1

@@ -1,7 +1,7 @@

11m_add : Maybe Int -> Maybe Int -> Maybe Int

22m_add x y = do x' <- x -- Extract value from x

33 y' <- y -- Extract value from y

4− return (x' + y') -- Add them

4+ pure (x' + y') -- Add them

66m_add' : Maybe Int -> Maybe Int -> Maybe Int

77m_add' x y = [ x' + y' | x' <- x, y' <- y ]