From 9e0bbf735156c83d387bd463a44d0d2e0f747baf Mon Sep 17 00:00:00 2001 From: janmasrovira Date: Wed, 14 Sep 2022 14:31:28 +0200 Subject: [PATCH] Replace -> by := in lambda syntax (#1533) --- src/Juvix/Compiler/Concrete/Pretty/Base.hs | 2 +- .../Concrete/Translation/FromSource.hs | 4 +- .../Concrete/Translation/FromSource/Lexer.hs | 7 ++-- src/Juvix/Compiler/Core/Pretty/Base.hs | 4 +- .../Compiler/Core/Translation/FromSource.hs | 14 +++---- .../Core/Translation/FromSource/Lexer.hs | 7 ++-- src/Juvix/Compiler/Internal/Pretty/Base.hs | 2 +- tests/Core/benchmark/test004.jvc | 6 +-- tests/Core/positive/test007.jvc | 8 ++-- tests/Core/positive/test012.jvc | 8 ++-- tests/Core/positive/test023.jvc | 16 ++++---- tests/Core/positive/test026.jvc | 18 ++++----- tests/Core/positive/test028.jvc | 24 ++++++------ tests/Core/positive/test029.jvc | 4 +- tests/Core/positive/test030.jvc | 8 ++-- tests/Core/positive/test033.jvc | 8 ++-- tests/Core/positive/test035.jvc | 38 +++++++++---------- tests/negative/BindGroupConflict/Lambda.juvix | 2 +- tests/positive/StdlibList/Data/List.juvix | 16 ++++---- 19 files changed, 97 insertions(+), 99 deletions(-) diff --git a/src/Juvix/Compiler/Concrete/Pretty/Base.hs b/src/Juvix/Compiler/Concrete/Pretty/Base.hs index 495c2c305..6718b9f91 100644 --- a/src/Juvix/Compiler/Concrete/Pretty/Base.hs +++ b/src/Juvix/Compiler/Concrete/Pretty/Base.hs @@ -482,7 +482,7 @@ instance SingI s => PrettyCode (LambdaClause s) where ppCode LambdaClause {..} = do lambdaParameters' <- hsep . toList <$> mapM ppPatternAtom lambdaParameters lambdaBody' <- ppExpression lambdaBody - return $ lambdaParameters' <+> kwMapsto <+> lambdaBody' + return $ lambdaParameters' <+> kwAssign <+> lambdaBody' instance SingI s => PrettyCode (Lambda s) where ppCode Lambda {..} = do diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs index 56d56353a..4c1488ab6 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource.hs @@ -471,7 +471,7 @@ whereClause = lambdaClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash, NameIdGen] r => ParsecS r (LambdaClause 'Parsed) lambdaClause = do lambdaParameters <- P.some patternAtom - kwMapsTo + kwAssign lambdaBody <- parseExpressionAtoms return LambdaClause {..} @@ -537,7 +537,7 @@ parsePatternAtoms = do functionClause :: Members '[Reader ParserParams, InfoTableBuilder, JudocStash, NameIdGen] r => Symbol -> ParsecS r (FunctionClause 'Parsed) functionClause _clauseOwnerFunction = do _clausePatterns <- P.many patternAtom - kwAssignment + kwAssign _clauseBody <- parseExpressionAtoms _clauseWhere <- optional whereBlock return FunctionClause {..} diff --git a/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs index 8ed631411..33170c111 100644 --- a/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs +++ b/src/Juvix/Compiler/Concrete/Translation/FromSource/Lexer.hs @@ -93,7 +93,7 @@ dottedIdentifier = lexeme $ P.sepBy1 bareIdentifier dot allKeywords :: Members '[Reader ParserParams, InfoTableBuilder] r => [ParsecS r ()] allKeywords = - [ kwAssignment, + [ kwAssign, kwAxiom, kwColon, kwColonOmega, @@ -112,7 +112,6 @@ allKeywords = kwInfixr, kwLambda, kwLet, - kwMapsTo, kwModule, kwOpen, kwPostfix, @@ -146,8 +145,8 @@ braces = between (symbol "{") (symbol "}") kwBuiltin :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwBuiltin = keyword Str.builtin -kwAssignment :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () -kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii +kwAssign :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () +kwAssign = keyword Str.assignUnicode <|> keyword Str.assignAscii kwAxiom :: Members '[Reader ParserParams, InfoTableBuilder] r => ParsecS r () kwAxiom = keyword Str.axiom diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs index 3474d6902..d481f2bfb 100644 --- a/src/Juvix/Compiler/Core/Pretty/Base.hs +++ b/src/Juvix/Compiler/Core/Pretty/Base.hs @@ -143,12 +143,12 @@ ppCodeCase' branchBinderNames branchTagNames Case {..} = do bns <- mapM (mapM (maybe (return kwQuestion) ppCode)) branchBinderNames cns <- zipWithM (\tag -> maybe (ppCode tag) ppCode) branchTags branchTagNames v <- ppCode _caseValue - bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwMapsto <+> br') cns bns branchBodies + bs' <- sequence $ zipWith3Exact (\cn bn br -> ppCode br >>= \br' -> return $ foldl' (<+>) cn bn <+> kwAssign <+> br') cns bns branchBodies bs'' <- case _caseDefault of Just def -> do d' <- ppCode def - return $ bs' ++ [kwDefault <+> kwMapsto <+> d'] + return $ bs' ++ [kwDefault <+> kwAssign <+> d'] Nothing -> return bs' let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs'' return $ kwCase <+> v <+> kwOf <+> bss diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs index 388b80aa7..215e1b489 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs @@ -156,7 +156,7 @@ parseDefinition :: Symbol -> ParsecS r () parseDefinition sym = do - kwAssignment + kwAssign node <- expression lift $ registerIdentNode sym node let (is, _) = unfoldLambdas node @@ -558,7 +558,7 @@ exprLetrecOne :: exprLetrecOne varsNum vars = do kwLetRec name <- parseLocalName - kwAssignment + kwAssign let vars' = HashMap.insert (name ^. nameText) varsNum vars value <- expr (varsNum + 1) vars' kwIn @@ -599,7 +599,7 @@ letrecDefs names varsNum vars = case names of when (n /= txt) $ parseFailure off "identifier name doesn't match letrec signature" name <- lift $ freshName KNameLocal txt i - kwAssignment + kwAssign v <- expr varsNum vars if | null names' -> optional kwSemicolon >> kwIn @@ -615,7 +615,7 @@ letrecDef :: letrecDef varsNum vars = do (txt, i) <- identifierL name <- lift $ freshName KNameLocal txt i - kwAssignment + kwAssign v <- expr varsNum vars return (name, v) @@ -627,7 +627,7 @@ exprLet :: exprLet varsNum vars = do kwLet name <- parseLocalName - kwAssignment + kwAssign value <- expr varsNum vars kwIn let vars' = HashMap.insert (name ^. nameText) varsNum vars @@ -682,7 +682,7 @@ defaultBranch :: ParsecS r Node defaultBranch varsNum vars = do kwWildcard - kwMapsTo + kwAssign expr varsNum vars matchingBranch :: @@ -704,7 +704,7 @@ matchingBranch varsNum vars = do when (ci ^. constructorArgsNum /= bindersNum) (parseFailure off "wrong number of constructor arguments") - kwMapsTo + kwAssign let vars' = fst $ foldl' diff --git a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs index 9fc6a2e0c..47fd05b84 100644 --- a/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs +++ b/src/Juvix/Compiler/Core/Translation/FromSource/Lexer.hs @@ -52,7 +52,7 @@ bareIdentifier = rawIdentifier allKeywords allKeywords :: [ParsecS r ()] allKeywords = - [ kwAssignment, + [ kwAssign, kwColon, kwLambda, kwLet, @@ -65,7 +65,6 @@ allKeywords = kwThen, kwElse, kwDef, - kwMapsTo, kwRightArrow, kwSemicolon, kwWildcard, @@ -103,8 +102,8 @@ parens = between lparen rparen braces :: ParsecS r a -> ParsecS r a braces = between (symbol "{") (symbol "}") -kwAssignment :: ParsecS r () -kwAssignment = keyword Str.assignUnicode <|> keyword Str.assignAscii +kwAssign :: ParsecS r () +kwAssign = keyword Str.assignUnicode <|> keyword Str.assignAscii kwColon :: ParsecS r () kwColon = keyword Str.colon diff --git a/src/Juvix/Compiler/Internal/Pretty/Base.hs b/src/Juvix/Compiler/Internal/Pretty/Base.hs index 9f071050f..999b555d2 100644 --- a/src/Juvix/Compiler/Internal/Pretty/Base.hs +++ b/src/Juvix/Compiler/Internal/Pretty/Base.hs @@ -44,7 +44,7 @@ instance PrettyCode Lambda where ppCode l = do b' <- ppCode (l ^. lambdaBody) v' <- ppCode (l ^. lambdaVar) - return $ kwLambda <+> braces (v' <+> kwMapsto <+> b') + return $ kwLambda <+> braces (v' <+> kwAssign <+> b') instance PrettyCode Application where ppCode a = do diff --git a/tests/Core/benchmark/test004.jvc b/tests/Core/benchmark/test004.jvc index 0e0b65ade..61cfa6bd8 100644 --- a/tests/Core/benchmark/test004.jvc +++ b/tests/Core/benchmark/test004.jvc @@ -7,7 +7,7 @@ def force := \f f nil; def filter := \p \s \_ case force s of { - cons h t -> + cons h t := if p h then cons h (filter p t) else @@ -16,7 +16,7 @@ def filter := \p \s \_ def nth := \n \s case force s of { - cons h t -> if n = 1 then h else nth (n - 1) t + cons h t := if n = 1 then h else nth (n - 1) t }; def numbers := \n \_ cons n (numbers (n + 1)); @@ -24,7 +24,7 @@ def numbers := \n \_ cons n (numbers (n + 1)); def indivisible := \n \x if x % n = 0 then false else true; def eratostenes := \s \_ case force s of { - cons n t -> + cons n t := cons n (eratostenes (filter (indivisible n) t)) }; def primes := eratostenes (numbers 2); diff --git a/tests/Core/positive/test007.jvc b/tests/Core/positive/test007.jvc index 45be90b85..ac5edcf2c 100644 --- a/tests/Core/positive/test007.jvc +++ b/tests/Core/positive/test007.jvc @@ -3,11 +3,11 @@ constr nil 0; constr cons 2; -def hd := \x case x of { cons x' _ -> x' }; -def tl := \x case x of { cons _ x' -> x' }; -def null := \x case x of { nil -> true; _ -> false }; +def hd := \x case x of { cons x' _ := x' }; +def tl := \x case x of { cons _ x' := x' }; +def null := \x case x of { nil := true; _ := false }; -def map := \f \x case x of { nil -> nil; cons h t -> cons (f h) (map f t) }; +def map := \f \x case x of { nil := nil; cons h t := cons (f h) (map f t) }; def map' := \f \x if null x then nil else cons (f (hd x)) (map' f (tl x)); def lst := cons 0 (cons 1 nil); diff --git a/tests/Core/positive/test012.jvc b/tests/Core/positive/test012.jvc index 9e0f27e63..0779d15eb 100644 --- a/tests/Core/positive/test012.jvc +++ b/tests/Core/positive/test012.jvc @@ -16,10 +16,10 @@ def gen := \n node3 (gen (n - 1)) (gen (n - 1)) (gen (n - 1)); def preorder := \t case t of { - node1 c -> write 1 >> preorder c; - node2 l r -> write 2 >> preorder l >> preorder r; - node3 l m r -> write 3 >> preorder l >> preorder m >> preorder r; - leaf -> write 0; + node1 c := write 1 >> preorder c; + node2 l r := write 2 >> preorder l >> preorder r; + node3 l m r := write 3 >> preorder l >> preorder m >> preorder r; + leaf := write 0; }; preorder (gen 3) >> write "\n" >> diff --git a/tests/Core/positive/test023.jvc b/tests/Core/positive/test023.jvc index 6f2d644d3..8ef70a47d 100644 --- a/tests/Core/positive/test023.jvc +++ b/tests/Core/positive/test023.jvc @@ -3,16 +3,16 @@ constr nil 0; constr cons 2; -def head := \l case l of { cons h _ -> h }; -def tail := \l case l of { cons _ t -> t }; -def null := \l case l of { nil -> true; cons _ _ -> false }; -def map := \f \l case l of { nil -> nil; cons h t -> cons (f h) (map f t) }; -def foldl := \f \acc \l case l of { nil -> acc; cons h t -> foldl f (f acc h) t }; -def foldr := \f \acc \l case l of { nil -> acc; cons h t -> f h (foldr f acc t) }; +def head := \l case l of { cons h _ := h }; +def tail := \l case l of { cons _ t := t }; +def null := \l case l of { nil := true; cons _ _ := false }; +def map := \f \l case l of { nil := nil; cons h t := cons (f h) (map f t) }; +def foldl := \f \acc \l case l of { nil := acc; cons h t := foldl f (f acc h) t }; +def foldr := \f \acc \l case l of { nil := acc; cons h t := f h (foldr f acc t) }; def filter := \f \l case l of { - nil -> nil; - cons h t -> + nil := nil; + cons h t := if f h then cons h (filter f t) else diff --git a/tests/Core/positive/test026.jvc b/tests/Core/positive/test026.jvc index a40507307..0353ae897 100644 --- a/tests/Core/positive/test026.jvc +++ b/tests/Core/positive/test026.jvc @@ -8,26 +8,26 @@ def gen := \n if n <= 0 then leaf else node (gen (n - 2)) (gen (n - 1)); def g; def f := \t case t of { - leaf -> 1; - node l r -> + leaf := 1; + node l r := let l := g l in let r := g r in let a := case l of { - leaf -> 0 - 3; - node l r -> f l + f r + leaf := 0 - 3; + node l r := f l + f r } in let b := case r of { - node l r -> f l + f r; - _ -> 2 + node l r := f l + f r; + _ := 2 } in a * b }; -def isNode := \t case t of { node _ _ -> true; _ -> false }; -def isLeaf := \t case t of { leaf -> true; _ -> false }; +def isNode := \t case t of { node _ _ := true; _ := false }; +def isLeaf := \t case t of { leaf := true; _ := false }; def g := \t if isLeaf t then t else case t of { - node l r -> if isNode l then r else node r l + node l r := if isNode l then r else node r l }; def writeLn := \x write x >> write "\n"; diff --git a/tests/Core/positive/test028.jvc b/tests/Core/positive/test028.jvc index ac6c683e3..211402a03 100644 --- a/tests/Core/positive/test028.jvc +++ b/tests/Core/positive/test028.jvc @@ -3,38 +3,38 @@ constr nil 0; constr cons 2; -def hd := \l case l of { cons x _ -> x }; -def tl := \l case l of { cons _ x -> x }; +def hd := \l case l of { cons x _ := x }; +def tl := \l case l of { cons _ x := x }; def rev' := \l \acc case l of { - nil -> acc; - cons h t -> rev' t (cons h acc) + nil := acc; + cons h t := rev' t (cons h acc) }; def rev := \l rev' l nil; constr queue 2; -def fst := \q case q of { queue x _ -> x }; -def snd := \q case q of { queue _ x -> x }; +def fst := \q case q of { queue x _ := x }; +def snd := \q case q of { queue _ x := x }; def front := \q hd (fst q); def pop_front := \q let q' := queue (tl (fst q)) (snd q) in case fst q' of { - nil -> queue (rev (snd q')) nil; - _ -> q' + nil := queue (rev (snd q')) nil; + _ := q' }; def push_back := \q \x case fst q of { - nil -> queue (cons x nil) (snd q); - _ -> queue (fst q) (cons x (snd q)) + nil := queue (cons x nil) (snd q); + _ := queue (fst q) (cons x (snd q)) }; def is_empty := \q case fst q of { - nil -> case snd q of { nil -> true; _ -> false }; - _ -> false + nil := case snd q of { nil := true; _ := false }; + _ := false }; def empty := queue nil nil; diff --git a/tests/Core/positive/test029.jvc b/tests/Core/positive/test029.jvc index aa1919e8c..0200d5541 100644 --- a/tests/Core/positive/test029.jvc +++ b/tests/Core/positive/test029.jvc @@ -2,8 +2,8 @@ constr pair 2; -def fst := \p case p of { pair x _ -> x }; -def snd := \p case p of { pair _ x -> x }; +def fst := \p case p of { pair x _ := x }; +def snd := \p case p of { pair _ x := x }; def compose := \f \g \x f (g x); diff --git a/tests/Core/positive/test030.jvc b/tests/Core/positive/test030.jvc index 744aefbc7..43554897e 100644 --- a/tests/Core/positive/test030.jvc +++ b/tests/Core/positive/test030.jvc @@ -7,7 +7,7 @@ def force := \f f nil; def filter := \p \s \_ case force s of { - cons h t -> + cons h t := if p h then cons h (filter p t) else @@ -19,12 +19,12 @@ def take := \n \s nil else case force s of { - cons h t -> cons h (take (n - 1) t) + cons h t := cons h (take (n - 1) t) }; def nth := \n \s case force s of { - cons h t -> if n = 0 then h else nth (n - 1) t + cons h t := if n = 0 then h else nth (n - 1) t }; def numbers := \n \_ cons n (numbers (n + 1)); @@ -32,7 +32,7 @@ def numbers := \n \_ cons n (numbers (n + 1)); def indivisible := \n \x if x % n = 0 then false else true; def eratostenes := \s \_ case force s of { - cons n t -> + cons n t := cons n (eratostenes (filter (indivisible n) t)) }; def primes := eratostenes (numbers 2); diff --git a/tests/Core/positive/test033.jvc b/tests/Core/positive/test033.jvc index b1c430862..9c2e6bf85 100644 --- a/tests/Core/positive/test033.jvc +++ b/tests/Core/positive/test033.jvc @@ -7,13 +7,13 @@ def mklst := \n if n = 0 then nil else cons n (mklst (n - 1)); def mklst2 := \n if n = 0 then nil else cons (mklst n) (mklst2 (n - 1)); def append := \xs \ys case xs of { - nil -> ys; - cons x xs' -> cons x (append xs' ys); + nil := ys; + cons x xs' := cons x (append xs' ys); }; def flatten := \xs case xs of { - nil -> nil; - cons x xs' -> append x (flatten xs'); + nil := nil; + cons x xs' := append x (flatten xs'); }; def writeLn := \x write x >> write "\n"; diff --git a/tests/Core/positive/test035.jvc b/tests/Core/positive/test035.jvc index d3d357438..bc24141b2 100644 --- a/tests/Core/positive/test035.jvc +++ b/tests/Core/positive/test035.jvc @@ -6,8 +6,8 @@ constr cons 2; constr pair 2; def length := \xs case xs of { - nil -> 0; - cons _ xs' -> length xs' + 1 + nil := 0; + cons _ xs' := length xs' + 1 }; def split := \n \xs @@ -15,18 +15,18 @@ def split := \n \xs pair nil xs else case xs of { - nil -> pair nil nil; - cons x xs' -> + nil := pair nil nil; + cons x xs' := case split (n - 1) xs' of { - pair l1 l2 -> pair (cons x l1) l2 + pair l1 l2 := pair (cons x l1) l2 } }; def merge := \xs \ys case xs of { - nil -> ys; - cons x xs' -> case ys of { - nil -> xs; - cons y ys' -> + nil := ys; + cons x xs' := case ys of { + nil := xs; + cons y ys' := if x <= y then cons x (merge xs' ys) else @@ -40,14 +40,14 @@ def sort := \xs xs else case split (length xs / 2) xs of { - pair l1 l2 -> merge (sort l1) (sort l2) + pair l1 l2 := merge (sort l1) (sort l2) }; def uniq := \xs case xs of { - nil -> nil; - cons x xs' -> case xs' of { - nil -> xs; - cons x' _ -> + nil := nil; + cons x xs' := case xs' of { + nil := xs; + cons x' _ := if x = x' then uniq xs' else @@ -56,13 +56,13 @@ def uniq := \xs case xs of { }; def append := \xs \ys case xs of { - nil -> ys; - cons x xs' -> cons x (append xs' ys); + nil := ys; + cons x xs' := cons x (append xs' ys); }; def flatten := \xs case xs of { - nil -> nil; - cons x xs' -> append x (flatten xs'); + nil := nil; + cons x xs' := append x (flatten xs'); }; def take := \n \xs @@ -70,7 +70,7 @@ def take := \n \xs nil else case xs of { - cons x xs' -> cons x (take (n - 1) xs') + cons x xs' := cons x (take (n - 1) xs') }; def gen := \n \f \acc if n = 0 then acc else gen (n - 1) f (cons (f n) acc); diff --git a/tests/negative/BindGroupConflict/Lambda.juvix b/tests/negative/BindGroupConflict/Lambda.juvix index c73c96e7a..7aec355f1 100644 --- a/tests/negative/BindGroupConflict/Lambda.juvix +++ b/tests/negative/BindGroupConflict/Lambda.juvix @@ -5,6 +5,6 @@ module Lambda; }; fst : (a : Type) → (b : Type) → Pair a b → a ; - fst ≔ λ { _ _ (mkPair _ _ x x) ↦ x }; + fst ≔ λ { _ _ (mkPair _ _ x x) := x }; end; diff --git a/tests/positive/StdlibList/Data/List.juvix b/tests/positive/StdlibList/Data/List.juvix index c5a00ae2c..1d8c132ea 100644 --- a/tests/positive/StdlibList/Data/List.juvix +++ b/tests/positive/StdlibList/Data/List.juvix @@ -27,8 +27,8 @@ map a b f (∷ _ h hs) ≔ ∷ a (f h) (map a b f hs); filter : (a : Type) → (a → Bool) → List a → List a; filter a f (nil _) ≔ nil a; filter a f (∷ _ h hs) ≔ match (f h) λ{ - true ↦ ∷ a h (filter a f hs); - false ↦ filter a f hs; + true := ∷ a h (filter a f hs); + false := filter a f hs; }; import Data.Nat; @@ -64,14 +64,14 @@ splitAt : (a : Type) → ℕ → List a → List a; splitAt a _ (nil _) ≔ nil a, nil a; splitAt a zero xs ≔ , (List a) (List a) (nil a) xs; splitAt a (suc zero) (∷ _ x xs) ≔ , (List a) (List a) (∷ a x (nil a)) xs; -splitAt a (suc (suc m)) (∷ _ x xs) ≔ match (splitAt a m xs) λ{ - (, la _ xs' xs'') ↦ , la la (∷ a x xs') xs''; +splitAt a (suc (suc m)) (∷ _ x xs) ≔ match (splitAt a m xs) λ { + (, la _ xs' xs'') := , la la (∷ a x xs') xs''; }; merge : (a : Type) → (a → a → Ordering) → List a → List a → List a; merge a cmp (∷ _ x xs) (∷ _ y ys) ≔ match (cmp x y) λ{ - LT ↦ ∷ a x (merge a cmp xs (∷ a y ys)); - _ ↦ ∷ a y (merge a cmp (∷ a x xs) ys); + LT := ∷ a x (merge a cmp xs (∷ a y ys)); + _ := ∷ a y (merge a cmp (∷ a x xs) ys); }; merge _ _ (nil _) ys ≔ ys; merge _ _ xs (nil _) ≔ xs; @@ -90,8 +90,8 @@ quickSort a cmp (∷ _ x ys) ≔ where { ltx : a → Bool; ltx y ≔ match (cmp y x) λ{ - LT ↦ true; - _ ↦ false; + LT := true; + _ := false; }; gex : a → Bool; gex y ≔ not (ltx y)