From 41daf19e01dd785b1a06b0ddd5b0ddc79522439e Mon Sep 17 00:00:00 2001 From: Lukasz Czajka Date: Mon, 4 Nov 2024 13:06:49 +0100 Subject: [PATCH] update to new record update scoping rules --- Data/Debug.juvix | 3 +-- Example.juvix | 2 +- Package.juvix | 2 +- Test/QuickCheck/Testable.juvix | 2 +- juvix.lock.yaml | 4 ++-- 5 files changed, 6 insertions(+), 7 deletions(-) diff --git a/Data/Debug.juvix b/Data/Debug.juvix index 20c8279..335c23e 100644 --- a/Data/Debug.juvix +++ b/Data/Debug.juvix @@ -1,4 +1,3 @@ module Data.Debug; -terminating -undefined : {A : Type} -> A := undefined; +axiom undefined : {A : Type} -> A; diff --git a/Example.juvix b/Example.juvix index 503f7f7..f388978 100644 --- a/Example.juvix +++ b/Example.juvix @@ -13,7 +13,7 @@ prop-reverseDoesNotChangeLength (xs : List Int) : Bool := length (reverse xs) == prop-reverseReverseIsIdentity (xs : List Int) : Bool := eqListInt xs (reverse (reverse xs)); prop-tailLengthOneLess (xs : List Int) : Bool := - null xs || ofNat (length (tail xs)) == intSubNat (length xs) 1; + isEmpty xs || ofNat (length (tail xs)) == intSubNat (length xs) 1; prop-splitAtRecombine (n : Nat) (xs : List Int) : Bool := case splitAt n xs of lhs, rhs := eqListInt xs (lhs ++ rhs); diff --git a/Package.juvix b/Package.juvix index b764c74..be41914 100644 --- a/Package.juvix +++ b/Package.juvix @@ -6,6 +6,6 @@ package : Package := defaultPackage@?{ name := "quickcheck"; version := mkVersion 0 15 0; - dependencies := [github "anoma" "juvix-stdlib" "1e581bb8fb8a6a9198ad927d1611d280ad5789a6"]; + dependencies := [github "anoma" "juvix-stdlib" "ca916cf56258396cc1c559cebf355106b6de199d"]; main := just "Example.juvix" }; diff --git a/Test/QuickCheck/Testable.juvix b/Test/QuickCheck/Testable.juvix index 1c22ba2..054a9fd 100644 --- a/Test/QuickCheck/Testable.juvix +++ b/Test/QuickCheck/Testable.juvix @@ -26,7 +26,7 @@ forAll {A T : Type} {{Show A}} {{Arbitrary A}} {{Testable T}} : (A -> T) -> Prop res : Outcome := runProp subProp rand2; in overFailure res - \ {f := f@Failure{counterExamples := Show.show arg :: counterExamples}}}); + \ {f := f@Failure{counterExamples := Show.show arg :: Failure.counterExamples f}}}); instance testableProperty : Testable Property := mkTestable id; diff --git a/juvix.lock.yaml b/juvix.lock.yaml index 6e7ce47..2ea5ec6 100644 --- a/juvix.lock.yaml +++ b/juvix.lock.yaml @@ -2,10 +2,10 @@ # Do not edit this file manually. version: 2 -checksum: 3ac97b0abcbe0af531a71551a177ed89935e3c5b348f802db106b30d41075583 +checksum: 71ea35a8c53a5d4e1e3760283204278e0006aa20b260468f8e6cf28fd8d94666 dependencies: - git: name: anoma_juvix-stdlib - ref: 1e581bb8fb8a6a9198ad927d1611d280ad5789a6 + ref: ca916cf56258396cc1c559cebf355106b6de199d url: https://github.com/anoma/juvix-stdlib dependencies: []