From f0b5536df14b24cc47fe004390b0dbfe907ec4f7 Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Tue, 19 Nov 2024 11:59:09 +0100 Subject: [PATCH] fix formatting --- src/Juvix/Compiler/Concrete/Print/Base.hs | 6 +++--- tests/positive/TypeSignatures.juvix | 10 ++++++---- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Print/Base.hs b/src/Juvix/Compiler/Concrete/Print/Base.hs index 7e00217022..fa30dbc2a8 100644 --- a/src/Juvix/Compiler/Concrete/Print/Base.hs +++ b/src/Juvix/Compiler/Concrete/Print/Base.hs @@ -1095,7 +1095,7 @@ instance (SingI s) => PrettyPrint (AxiomDef s) where ?<> builtin' ?<> ppCode _axiomKw <+> axiomName' - <+> ppCode _axiomTypeSig + <> ppCode _axiomTypeSig instance PrettyPrint BuiltinInductive where ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i) @@ -1433,7 +1433,7 @@ instance (SingI s) => PrettyPrint (RecordField s) where ?<> pragmas' ?<> builtin' ?<> mayBraces (ppSymbolType _fieldName) - <+> ppCode _fieldTypeSig + <> ppCode _fieldTypeSig instance (SingI s) => PrettyPrint (RhsRecord s) where ppCode RhsRecord {..} = do @@ -1466,7 +1466,7 @@ ppConstructorDef singleConstructor ConstructorDef {..} = do constructorRhsHelper r = spaceMay <> ppCode r where spaceMay = case r of - ConstructorRhsGadt {} -> space + ConstructorRhsGadt {} -> mempty ConstructorRhsRecord {} -> mempty ConstructorRhsAdt a | null (a ^. rhsAdtArguments) -> mempty diff --git a/tests/positive/TypeSignatures.juvix b/tests/positive/TypeSignatures.juvix index 0378dd1ce8..18fdcd4706 100644 --- a/tests/positive/TypeSignatures.juvix +++ b/tests/positive/TypeSignatures.juvix @@ -5,10 +5,12 @@ import Stdlib.Data.Nat open; axiom f (x : Nat) : Nat; g (x : Nat) : Nat := - f@{x := x}; + f@{ + x := x; + }; -type R := mkR@{ - rf (x : Nat) : Nat; -}; +type R := mkR@{rf (x : Nat) : Nat}; type R' := mkR' (rf : Nat -> Nat) : R'; + +type RR := mkRR : (Nat -> Nat) -> RR;