mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-01 01:09:03 +03:00
Add indentation checks when parsing args in implDecl
This commit is contained in:
parent
03d6c5f637
commit
1142f73e05
@ -1607,7 +1607,7 @@ implDecl fname indents
|
||||
impls <- implBinds fname indents
|
||||
cons <- constraints fname indents
|
||||
n <- decorate fname Typ name
|
||||
params <- many (simpleExpr fname indents)
|
||||
params <- many (continue indents *> simpleExpr fname indents)
|
||||
nusing <- option [] $ decoratedKeyword fname "using"
|
||||
*> forget <$> some (decorate fname Function name)
|
||||
body <- optional $ decoratedKeyword fname "where" *> blockAfter col (topDecl fname)
|
||||
|
@ -92,7 +92,7 @@ idrisTestsError = MkTestPool "Error messages" [] Nothing
|
||||
"perror001", "perror002", "perror003", "perror004", "perror005",
|
||||
"perror006", "perror007", "perror008", "perror009", "perror010",
|
||||
"perror011", "perror012", "perror013", "perror014", "perror015",
|
||||
"perror016"]
|
||||
"perror016", "perror017"]
|
||||
|
||||
idrisTestsInteractive : TestPool
|
||||
idrisTestsInteractive = MkTestPool "Interactive editing" [] Nothing
|
||||
|
13
tests/idris2/perror017/ParseImpl.idr
Normal file
13
tests/idris2/perror017/ParseImpl.idr
Normal file
@ -0,0 +1,13 @@
|
||||
import Control.Monad.Identity
|
||||
|
||||
|
||||
interface Functor' (0 f :Type -> Type) where
|
||||
map': (a -> b) -> f a -> f b
|
||||
|
||||
Product' : (Type -> Type) -> (Type -> Type) -> (Type -> Type -> Type)
|
||||
Product' f g = (\a, b => (f a, g b))
|
||||
|
||||
[prod] Functor' f => Functor' g => Functor' ((Product' f g) a)
|
||||
|
||||
Functor' Identity where
|
||||
map' f (Id x) = Id (f x)
|
1
tests/idris2/perror017/expected
Normal file
1
tests/idris2/perror017/expected
Normal file
@ -0,0 +1 @@
|
||||
1/1: Building ParseImpl (ParseImpl.idr)
|
3
tests/idris2/perror017/run
Executable file
3
tests/idris2/perror017/run
Executable file
@ -0,0 +1,3 @@
|
||||
rm -rf build
|
||||
|
||||
$1 --no-color --console-width 0 --check ParseImpl.idr || true
|
Loading…
Reference in New Issue
Block a user