diff --git a/src/Juvix/Parser/Lexer.hs b/src/Juvix/Parser/Lexer.hs index c1268e47a6..518f96c995 100644 --- a/src/Juvix/Parser/Lexer.hs +++ b/src/Juvix/Parser/Lexer.hs @@ -119,7 +119,7 @@ space' special = | otherwise -> return (acc <> pack txt) integerWithBase' :: ParsecS r (WithLoc IntegerWithBase) -integerWithBase' = withLoc $ do +integerWithBase' = P.try $ withLoc $ do minus <- optional (char '-') b <- integerBase' num :: Integer <- case b of diff --git a/tests/Core/positive/test043.jvc b/tests/Core/positive/test043.jvc index 7adfb28e3d..512087a7f8 100644 --- a/tests/Core/positive/test043.jvc +++ b/tests/Core/positive/test043.jvc @@ -2,32 +2,32 @@ def fun : Π A : Type, - A → A := + A -> A := λ(A : Type) λ(x : A) - let f : (A → A) → A := λ(h : A → A) h (h x) in + let f : (A -> A) -> A := λ(h : A -> A) h (h x) in f (λ(y : A) x); -def helper : Int → Int → Int := +def helper : Int -> Int -> Int := λ(a : Int) λ(b : Int) a * b - b; -def fun' : Π T : Type → Type, +def fun' : Π T : Type -> Type, Π unused : Type, Π C : Type, Π A : Type, - (T A → A → C) - → A - → C := - λ(T : Type → Type) + (T A -> A -> C) + -> A + -> C := + λ(T : Type -> Type) λ(unused : Type) λ(C : Type) λ(A : Type) - λ(mhelper : T A → A → C) + λ(mhelper : T A -> A -> C) λ(a' : A) - let f : (A → A) → A := λ(g : A → A) g (g a') in - let h : A → A → C := λ(a1 : A) λ(a2 : A) mhelper a2 a1 in + let f : (A -> A) -> A := λ(g : A -> A) g (g a') in + let h : A -> A -> C := λ(a1 : A) λ(a2 : A) mhelper a2 a1 in f (λ(y : A) h y a'); fun Int 2 + fun' (λ(A : Type) A) Bool Int Int helper 3 diff --git a/tests/Internal/positive/out/FunctionType.out b/tests/Internal/positive/out/FunctionType.out index 1e3bf3207c..644b032a97 100644 --- a/tests/Internal/positive/out/FunctionType.out +++ b/tests/Internal/positive/out/FunctionType.out @@ -1 +1 @@ -Π A : Type, Π B : Type, A → B +Π A : Type, Π B : Type, A -> B