mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-21 02:07:25 +03:00
Fix #616
This commit is contained in:
parent
d56b090c4c
commit
7de26e7d75
@ -662,7 +662,7 @@ mutual
|
||||
("do" :: ns) =>
|
||||
do actions <- bounds (block (doAct fname))
|
||||
pure (PDoBlock (boundToFC fname (mergeBounds nsdo actions))
|
||||
(Just (reverse ns)) (concat actions.val))
|
||||
(Just ns) (concat actions.val))
|
||||
_ => fail "Not a namespaced 'do'"
|
||||
|
||||
lowerFirst : String -> Bool
|
||||
|
@ -7,3 +7,21 @@ foo : IO ()
|
||||
foo = MyDo.do
|
||||
x <- "Silly"
|
||||
putStrLn x
|
||||
|
||||
namespace A
|
||||
namespace B
|
||||
export
|
||||
(>>=) : Nat -> (() -> Nat) -> Nat
|
||||
(>>=) x fy = x + (fy ())
|
||||
|
||||
test : Nat
|
||||
test = B.A.do
|
||||
5
|
||||
6
|
||||
7
|
||||
|
||||
test2 : Nat
|
||||
test2 = A.B.do
|
||||
5
|
||||
6
|
||||
7
|
||||
|
@ -1 +1,8 @@
|
||||
1/1: Building QDo (QDo.idr)
|
||||
Error: While processing right hand side of test. Undefined name B.A.>>=.
|
||||
|
||||
QDo.idr:19:10--19:11
|
||||
|
|
||||
19 | 5
|
||||
| ^
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user