diff --git a/tests/Casm/Compilation/positive/test026.juvix b/tests/Casm/Compilation/positive/test026.juvix index c559ec68a3..f3cc2b1a6c 100644 --- a/tests/Casm/Compilation/positive/test026.juvix +++ b/tests/Casm/Compilation/positive/test026.juvix @@ -3,8 +3,7 @@ module test026; import Stdlib.Prelude open; -type Queue (A : Type) := - | queue : List A → List A → Queue A; +type Queue (A : Type) := queue : List A → List A → Queue A; qfst : {A : Type} → Queue A → List A | (queue x _) := x; @@ -19,9 +18,9 @@ pop_front : {A : Type} → Queue A → Queue A | {A} q := let q' : Queue A := queue (tail (qfst q)) (qsnd q); - in case qfst q' - | nil := queue (reverse (qsnd q')) nil - | _ := q'; + in case qfst q' of + | nil := queue (reverse (qsnd q')) nil + | _ := q'; push_back : {A : Type} → Queue A → A → Queue A | q x := @@ -33,9 +32,10 @@ is_empty : {A : Type} → Queue A → Bool | q := case qfst q of | nil := - (case qsnd q + case qsnd q of { | nil := true - | _ := false) + | _ := false + } | _ := false; empty : {A : Type} → Queue A := queue nil nil; @@ -45,8 +45,6 @@ g {{Partial}} : List Nat → Queue Nat → List Nat | acc q := if (is_empty q) acc (g (front q :: acc) (pop_front q)); --- TODO: remove `terminating` after fixing https://github.com/anoma/juvix/issues/2414 -terminating f {{Partial}} : Nat → Queue Nat → List Nat | zero q := g nil q | n@(suc n') q := f n' (push_back q n); @@ -55,4 +53,4 @@ sum : List Nat → Nat | nil := 0 | (h :: t) := h + sum t; -main : Nat := sum (runPartial (λ {{{_}} := f 100 empty})); +main : Nat := sum (runPartial λ {{{_}} := f 100 empty});