mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 22:17:19 +03:00
Treat (=) as a special function name.
Includes a regression test. Fixes #884
This commit is contained in:
parent
af082b6f0d
commit
be7d600f0d
@ -82,12 +82,16 @@ backtick = Infix (do indentPropHolds gtProp
|
||||
optional namespace
|
||||
|
||||
@
|
||||
OperatorFront ::= (Identifier_t '.')? '(' Operator_t ')';
|
||||
OperatorFront ::=
|
||||
'(' '=' ')'
|
||||
| (Identifier_t '.')? '(' Operator_t ')'
|
||||
;
|
||||
@
|
||||
|
||||
-}
|
||||
operatorFront :: IdrisParser Name
|
||||
operatorFront = maybeWithNS (lchar '(' *> operator <* lchar ')') False []
|
||||
operatorFront = try ((lchar '(' *> reservedOp "=" <* lchar ')') >> (return eqTy))
|
||||
<|> maybeWithNS (lchar '(' *> operator <* lchar ')') False []
|
||||
|
||||
{- | Parses a function (either normal name or operator)
|
||||
|
||||
|
0
test/reg037/expected
Normal file
0
test/reg037/expected
Normal file
9
test/reg037/reg037.idr
Normal file
9
test/reg037/reg037.idr
Normal file
@ -0,0 +1,9 @@
|
||||
|
||||
--- Parser regression for (=) as a function name (fnName)
|
||||
|
||||
class Foo (t : (A : Type) -> (B : Type) -> A -> B -> Type) where
|
||||
foo : (A : Type) -> (B : Type) -> (x : A) -> (y : B) -> t A B x y -> t A B x y
|
||||
|
||||
instance Foo (=) where
|
||||
foo A B x y prf = prf
|
||||
|
3
test/reg037/run
Executable file
3
test/reg037/run
Executable file
@ -0,0 +1,3 @@
|
||||
#!/usr/bin/env bash
|
||||
idris --check reg037.idr
|
||||
rm -f reg037 *.ibc
|
Loading…
Reference in New Issue
Block a user