mirror of
https://github.com/anoma/juvix.git
synced 2025-01-03 21:14:16 +03:00
Add negative test for AppLeftImplicit error (#154)
This commit is contained in:
parent
9eeeb0f95b
commit
b09d4602e7
@ -24,7 +24,7 @@ testDescr NegTest {..} =
|
||||
_testRoot = tRoot,
|
||||
_testAssertion = Single $ do
|
||||
let entryPoint = defaultEntryPoint _file
|
||||
res <- runIOEither (upToScoping entryPoint)
|
||||
res <- runIOEither (upToAbstract entryPoint)
|
||||
case mapLeft fromMiniJuvixError res of
|
||||
Left (Just err) -> whenJust (_checkErr err) assertFailure
|
||||
Left Nothing -> assertFailure "The scope checker did not find an error."
|
||||
@ -175,6 +175,13 @@ tests =
|
||||
$ \case
|
||||
ErrWrongLocationCompileBlock {} -> Nothing
|
||||
_ -> wrongError,
|
||||
NegTest
|
||||
"Implicit argument on the left of an application"
|
||||
"."
|
||||
"AppLeftImplicit.mjuvix"
|
||||
$ \case
|
||||
ErrAppLeftImplicit {} -> Nothing
|
||||
_ -> wrongError,
|
||||
NegTest
|
||||
"Multiple compile blocks for the same name"
|
||||
"CompileBlocks"
|
||||
|
6
tests/negative/AppLeftImplicit.mjuvix
Normal file
6
tests/negative/AppLeftImplicit.mjuvix
Normal file
@ -0,0 +1,6 @@
|
||||
module AppLeftImplicit;
|
||||
|
||||
x : Type;
|
||||
x ≔ {x};
|
||||
|
||||
end;
|
Loading…
Reference in New Issue
Block a user