mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-11-13 07:26:59 +03:00
Forgot to commit the update test...
This commit is contained in:
parent
f733bf0e30
commit
6c133a035a
@ -10,3 +10,19 @@ When elaborating an application of function Prelude.Monad.>>=:
|
||||
List
|
||||
with
|
||||
\{uv0} => argTy -> uv
|
||||
./baddoublebang.idr:6:26: error: not
|
||||
a terminator, expected: "$",
|
||||
"$>", "&&", "*", "+", "++", "-",
|
||||
"->", ".", "/", "/=", "::", ";",
|
||||
"<", "<#>", "<$", "<$>", "<*>",
|
||||
"<+>", "<->", "<<", "<=", "<|>",
|
||||
"=", "==", ">", ">=", ">>",
|
||||
">>=", "\\\\", "`", "in", "||",
|
||||
"~=~",
|
||||
ambiguous use of a left-associative operator,
|
||||
ambiguous use of a non-associative operator,
|
||||
ambiguous use of a right-associative operator,
|
||||
end of input, function argument,
|
||||
matching application expression
|
||||
doubleBang mmn = do pure !!mmn
|
||||
^
|
||||
|
Loading…
Reference in New Issue
Block a user