@@ -10,19 +10,3 @@ When elaborating an application of function Prelude.Monad.>>=:
1010 List
1111 with
1212 \{uv0} => argTy -> uv
13−./baddoublebang.idr:6:26: error: not
14− a terminator, expected: "$",
15− "$>", "&&", "*", "+", "++", "-",
16− "->", ".", "/", "/=", "::", ";",
17− "<", "<#>", "<$", "<$>", "<*>",
18− "<+>", "<->", "<<", "<=", "<|>",
19− "=", "==", ">", ">=", ">>",
20− ">>=", "@", "\\\\", "`", "in",
21− "||", "~=~",
22− ambiguous use of a left-associative operator,
23− ambiguous use of a non-associative operator,
24− ambiguous use of a right-associative operator,
25− end of input, function argument,
26− matching application expression
27−doubleBang mmn = do pure !!mmn
28− ^