mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-11 08:55:23 +03:00
Remove deprecated calls to return
This commit is contained in:
parent
8ea8a3858c
commit
a59677632a
@ -20,13 +20,13 @@ testTree = Node (Node Leaf "Jim" Leaf)
|
||||
(Node Leaf "Bob" Leaf))
|
||||
|
||||
treeTagAux : BTree a -> { [STATE Int] } Eff (BTree (Int, a))
|
||||
treeTagAux Leaf = return Leaf
|
||||
treeTagAux Leaf = pure Leaf
|
||||
treeTagAux (Node l x r)
|
||||
= do l' <- treeTagAux l
|
||||
i <- get
|
||||
put (i + 1)
|
||||
r' <- treeTagAux r
|
||||
return (Node l' (i, x) r')
|
||||
pure (Node l' (i, x) r')
|
||||
|
||||
treeTag : (i : Int) -> BTree a -> BTree (Int, a)
|
||||
treeTag i x = runPure (do put i
|
||||
|
@ -1,7 +1,7 @@
|
||||
m_add : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add x y = do x' <- x -- Extract value from x
|
||||
y' <- y -- Extract value from y
|
||||
return (x' + y') -- Add them
|
||||
pure (x' + y') -- Add them
|
||||
|
||||
m_add' : Maybe Int -> Maybe Int -> Maybe Int
|
||||
m_add' x y = [ x' + y' | x' <- x, y' <- y ]
|
||||
|
Loading…
Reference in New Issue
Block a user