From 9210d010c586f9593c42cddd19c50c5ebaac0a4a Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 18 Nov 2024 15:10:41 +0300 Subject: [PATCH 1/5] [ new ] Quantity for proof in with-clauses --- CHANGELOG_NEXT.md | 2 ++ libs/base/Language/Reflection/TTImp.idr | 4 ++-- src/Idris/Desugar.idr | 2 +- src/Idris/Parser.idr | 5 +++-- src/Idris/REPL.idr | 4 ++-- src/Idris/Syntax.idr | 2 +- src/TTImp/Parser.idr | 4 +++- src/TTImp/ProcessDef.idr | 8 ++++---- src/TTImp/TTImp.idr | 8 ++++---- tests/idris2/with/with012/WithProof0.idr | 20 ++++++++++++++++++++ tests/idris2/with/with012/WithProof1.idr | 23 +++++++++++++++++++++++ tests/idris2/with/with012/expected | 2 ++ tests/idris2/with/with012/run | 4 ++++ 13 files changed, 71 insertions(+), 17 deletions(-) create mode 100644 tests/idris2/with/with012/WithProof0.idr create mode 100644 tests/idris2/with/with012/WithProof1.idr create mode 100644 tests/idris2/with/with012/expected create mode 100755 tests/idris2/with/with012/run diff --git a/CHANGELOG_NEXT.md b/CHANGELOG_NEXT.md index 1f667c513dc..d50bfc635dc 100644 --- a/CHANGELOG_NEXT.md +++ b/CHANGELOG_NEXT.md @@ -76,6 +76,8 @@ This CHANGELOG describes the merged but unreleased changes. Please see [CHANGELO * Bind expressions in `do` blocks can now have a type ascription. See [#3327](https://github.com/idris-lang/Idris2/issues/3327). +* Added syntax to specifying quantity for proof in with-clause. + ### Compiler changes * The compiler now differentiates between "package search path" and "package diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index a902f995fd2..2146cd33f88 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -171,7 +171,7 @@ mutual PatClause : FC -> (lhs : TTImp) -> (rhs : TTImp) -> Clause WithClause : FC -> (lhs : TTImp) -> (rig : Count) -> (wval : TTImp) -> -- with'd expression (& quantity) - (prf : Maybe Name) -> -- optional name for the proof + (prf : Maybe (Count, Name)) -> -- optional name for the proof (& quantity) (flags : List WithFlag) -> List Clause -> Clause ImpossibleClause : FC -> (lhs : TTImp) -> Clause @@ -605,7 +605,7 @@ mutual showClause mode (WithClause fc lhs rig wval prf flags cls) -- TODO print flags = unwords [ show lhs, "with" - , showCount rig $ maybe id (\ nm => (++ " proof \{show nm}")) prf + , showCount rig $ maybe id (\ nm => (++ " proof \{showCount (fst nm) $ show (snd nm)}")) prf $ showParens True (show wval) , "{", joinBy "; " (assert_total $ map (showClause mode) cls), "}" ] diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index 54423d1816c..b1f70903b16 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -926,7 +926,7 @@ mutual {auto m : Ref MD Metadata} -> {auto o : Ref ROpts REPLOpts} -> List Name -> PWithProblem -> - Core (RigCount, RawImp, Maybe Name) + Core (RigCount, RawImp, Maybe (RigCount, Name)) desugarWithProblem ps (MkPWithProblem rig wval mnm) = (rig,,mnm) <$> desugar AnyExpr ps wval diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index 2655bc2607d..fa962e368d7 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -1222,8 +1222,9 @@ withProblem fname col indents = do rig <- multiplicity fname start <- mustWork $ bounds (decoratedSymbol fname "(") wval <- bracketedExpr fname start indents - prf <- optional (decoratedKeyword fname "proof" - *> UN . Basic <$> decoratedSimpleBinderName fname) + prf <- optional $ do + decoratedKeyword fname "proof" + pure (!(multiplicity fname), UN $ Basic !(decoratedSimpleBinderName fname)) pure (MkPWithProblem rig wval prf) mutual diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 3aabd8be094..e18989f802f 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -226,8 +226,8 @@ printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) cs <- traverse (printClause l (i + 2)) csraw pure (relit l ((pack (replicate i ' ') ++ show lhs - ++ " with " ++ elimSemi "0 " "1 " (const "") rig ++ "(" ++ show wval ++ ")" - ++ maybe "" (\ nm => " proof " ++ show nm) prf + ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")" + ++ maybe "" (\ nm => " proof " ++ showCount (fst nm) ++ show (snd nm)) prf ++ "\n")) ++ showSep "\n" cs) printClause l i (ImpossibleClause _ lhsraw) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index da89fc6df3e..ff84307e0c0 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -342,7 +342,7 @@ mutual constructor MkPWithProblem withRigCount : RigCount withRigValue : PTerm' nm - withRigProof : Maybe Name -- This ought to be a `Basic` username + withRigProof : Maybe (RigCount, Name) -- This ought to be a `Basic` username public export PClause : Type diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index f8806b04920..deb367ae55e 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -522,7 +522,9 @@ mutual symbol "(" wval <- expr fname indents symbol ")" - prf <- optional (keyword "proof" *> name) + prf <- optional $ do + keyword "proof" + pure (!(getMult !multiplicity), !name) ws <- nonEmptyBlock (clause (S withArgs) fname) end <- location let fc = MkFC fname start end diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 8786c0bcdcf..3fd6ebf62de 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -600,7 +600,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env Just _ => let fc = emptyFC in let refl = IVar fc (NS builtinNS (UN $ Basic "Refl")) in - [(mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)] + [(map snd mprf, INamedApp fc refl (UN $ Basic "x") wval_raw)] let rhs_in = gapply (IVar vfc wname) $ map (\ nm => (Nothing, IVar vfc nm)) envns @@ -633,7 +633,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env mkExplicit (b :: env) = b :: mkExplicit env bindWithArgs : - (rig : RigCount) -> (wvalTy : Term xs) -> Maybe (Name, Term xs) -> + (rig : RigCount) -> (wvalTy : Term xs) -> Maybe ((RigCount, Name), Term xs) -> (wvalEnv : Env Term xs) -> Core (ext : List Name ** ( Env Term (ext ++ xs) @@ -657,7 +657,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env in pure (wargs ** (scenv, var, binder)) - bindWithArgs {xs} rig wvalTy (Just (name, wval)) wvalEnv = do + bindWithArgs {xs} rig wvalTy (Just ((rigPrf, name), wval)) wvalEnv = do defs <- get Ctxt let eqName = NS builtinNS (UN $ Basic "Equal") @@ -689,7 +689,7 @@ checkClause {vars} mult vis totreq hashit n opts nest env binder : Term (wargs ++ xs) -> Term xs := \ t => Bind vfc wargn (Pi vfc rig Explicit wvalTy) - $ Bind vfc name (Pi vfc rig Implicit eqTy) t + $ Bind vfc name (Pi vfc rigPrf Implicit eqTy) t pure (wargs ** (scenv, var, binder)) diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 1a716264a3f..bed9d7ff5f4 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -427,7 +427,7 @@ mutual PatClause : FC -> (lhs : RawImp' nm) -> (rhs : RawImp' nm) -> ImpClause' nm WithClause : FC -> (lhs : RawImp' nm) -> (rig : RigCount) -> (wval : RawImp' nm) -> -- with'd expression (& quantity) - (prf : Maybe Name) -> -- optional name for the proof + (prf : Maybe (RigCount, Name)) -> -- optional name for the proof (flags : List WithFlag) -> List (ImpClause' nm) -> ImpClause' nm ImpossibleClause : FC -> (lhs : RawImp' nm) -> ImpClause' nm @@ -441,8 +441,8 @@ mutual = show lhs ++ " = " ++ show rhs show (WithClause fc lhs rig wval prf flags block) = show lhs - ++ " with (" ++ show rig ++ " " ++ show wval ++ ")" - ++ maybe "" (\ nm => " proof " ++ show nm) prf + ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")" + ++ maybe "" (\ nm => " proof " ++ showCount (fst nm) ++ show (snd nm)) prf ++ "\n\t" ++ show block show (ImpossibleClause fc lhs) = show lhs ++ " impossible" @@ -518,7 +518,7 @@ mutual export -mkWithClause : FC -> RawImp' nm -> List1 (RigCount, RawImp' nm, Maybe Name) -> +mkWithClause : FC -> RawImp' nm -> List1 (RigCount, RawImp' nm, Maybe (RigCount, Name)) -> List WithFlag -> List (ImpClause' nm) -> ImpClause' nm mkWithClause fc lhs ((rig, wval, prf) ::: []) flags cls = WithClause fc lhs rig wval prf flags cls diff --git a/tests/idris2/with/with012/WithProof0.idr b/tests/idris2/with/with012/WithProof0.idr new file mode 100644 index 00000000000..911ccae2df4 --- /dev/null +++ b/tests/idris2/with/with012/WithProof0.idr @@ -0,0 +1,20 @@ +module WithProof0 + +%default total + +%hide List.filter + +filter : (p : a -> Bool) -> (xs : List a) -> List a +filter p [] = [] +filter p (x :: xs) with (p x) + filter p (x :: xs) | False = filter p xs + filter p (x :: xs) | True = x :: filter p xs + + +filterSquared : (p : a -> Bool) -> (xs : List a) -> + filter p (filter p xs) === filter p xs +filterSquared p [] = Refl +filterSquared p (x :: xs) with (p x) proof 0 eq + filterSquared p (x :: xs) | False = filterSquared p xs -- easy + filterSquared p (x :: xs) | True + = rewrite eq in cong (x ::) (filterSquared p xs) diff --git a/tests/idris2/with/with012/WithProof1.idr b/tests/idris2/with/with012/WithProof1.idr new file mode 100644 index 00000000000..e0b5e81f2c7 --- /dev/null +++ b/tests/idris2/with/with012/WithProof1.idr @@ -0,0 +1,23 @@ +module WithProof1 + +%default total + +%hide List.filter + +filter : (p : a -> Bool) -> (xs : List a) -> List a +filter p [] = [] +filter p (x :: xs) with (p x) + filter p (x :: xs) | False = filter p xs + filter p (x :: xs) | True = x :: filter p xs + +consumeEq : (1 _ : x === y) -> () +consumeEq Refl = () + +filterSquared : (p : a -> Bool) -> (xs : List a) -> + filter p (filter p xs) === filter p xs +filterSquared p [] = Refl +filterSquared p (x :: xs) with (p x) proof 1 eq + filterSquared p (x :: xs) | False = case consumeEq eq of + () => filterSquared p xs + filterSquared p (x :: xs) | True = case consumeEq eq of + () => rewrite eq in cong (x ::) (filterSquared p xs) diff --git a/tests/idris2/with/with012/expected b/tests/idris2/with/with012/expected new file mode 100644 index 00000000000..21ab08ccd76 --- /dev/null +++ b/tests/idris2/with/with012/expected @@ -0,0 +1,2 @@ +1/1: Building WithProof0 (WithProof0.idr) +1/1: Building WithProof1 (WithProof1.idr) diff --git a/tests/idris2/with/with012/run b/tests/idris2/with/with012/run new file mode 100755 index 00000000000..b85c518ce0c --- /dev/null +++ b/tests/idris2/with/with012/run @@ -0,0 +1,4 @@ +. ../../../testutils.sh + +check WithProof0.idr +check WithProof1.idr From 13f08a9a53c9238b5c43917f8db62f9b229a6ab1 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 18 Nov 2024 16:12:45 +0300 Subject: [PATCH 2/5] [ test ] Add failing tests for quantities of proofs --- tests/idris2/with/with012/WithProof0Fail.idr | 28 ++++++++++++++++++++ tests/idris2/with/with012/WithProof1Fail.idr | 19 +++++++++++++ tests/idris2/with/with012/expected | 2 ++ tests/idris2/with/with012/run | 2 ++ 4 files changed, 51 insertions(+) create mode 100644 tests/idris2/with/with012/WithProof0Fail.idr create mode 100644 tests/idris2/with/with012/WithProof1Fail.idr diff --git a/tests/idris2/with/with012/WithProof0Fail.idr b/tests/idris2/with/with012/WithProof0Fail.idr new file mode 100644 index 00000000000..2cac831b57e --- /dev/null +++ b/tests/idris2/with/with012/WithProof0Fail.idr @@ -0,0 +1,28 @@ +module WithProof0Fail + +%default total + +%hide List.filter + +data So : Bool -> Type where + Oh : So True + +eqToSo : b = True -> So b +eqToSo Refl = Oh + +data All : (0 p : a -> Type) -> List a -> Type where + Nil : All p Nil + (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs) + +filter : (p : a -> Bool) -> (xs : List a) -> List a +filter p [] = [] +filter p (x :: xs) with (p x) + filter p (x :: xs) | False = filter p xs + filter p (x :: xs) | True = x :: filter p xs + +failing "While processing right hand side of with block in allFilter. prf is not accessible in this context" + allFilter : (p : a -> Bool) -> (xs : List a) -> All (So . p) (filter p xs) + allFilter p [] = [] + allFilter p (x :: xs) with (p x) proof 0 prf + allFilter p (x :: xs) | False = allFilter p xs + allFilter p (x :: xs) | True = eqToSo prf :: allFilter p xs diff --git a/tests/idris2/with/with012/WithProof1Fail.idr b/tests/idris2/with/with012/WithProof1Fail.idr new file mode 100644 index 00000000000..8d803f9c649 --- /dev/null +++ b/tests/idris2/with/with012/WithProof1Fail.idr @@ -0,0 +1,19 @@ +module WithProof1Fail + +%default total + +%hide List.filter + +filter : (p : a -> Bool) -> (xs : List a) -> List a +filter p [] = [] +filter p (x :: xs) with (p x) + filter p (x :: xs) | False = filter p xs + filter p (x :: xs) | True = x :: filter p xs + +failing "While processing right hand side of with block in filterSquared. There are 0 uses of linear name eq" + filterSquared : (p : a -> Bool) -> (xs : List a) -> + filter p (filter p xs) === filter p xs + filterSquared p [] = Refl + filterSquared p (x :: xs) with (p x) proof 1 eq + filterSquared p (x :: xs) | False = filterSquared p xs + filterSquared p (x :: xs) | True = filterSquared p xs diff --git a/tests/idris2/with/with012/expected b/tests/idris2/with/with012/expected index 21ab08ccd76..c90e84658d3 100644 --- a/tests/idris2/with/with012/expected +++ b/tests/idris2/with/with012/expected @@ -1,2 +1,4 @@ 1/1: Building WithProof0 (WithProof0.idr) 1/1: Building WithProof1 (WithProof1.idr) +1/1: Building WithProof0Fail (WithProof0Fail.idr) +1/1: Building WithProof1Fail (WithProof1Fail.idr) diff --git a/tests/idris2/with/with012/run b/tests/idris2/with/with012/run index b85c518ce0c..d0852365cc0 100755 --- a/tests/idris2/with/with012/run +++ b/tests/idris2/with/with012/run @@ -2,3 +2,5 @@ check WithProof0.idr check WithProof1.idr +check WithProof0Fail.idr +check WithProof1Fail.idr From e6d6114458ea97ce7cee28fe66f8673bf20d30d1 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Wed, 4 Dec 2024 15:17:56 +0300 Subject: [PATCH 3/5] [ cleanup ] Match on pairs --- libs/base/Language/Reflection/TTImp.idr | 3 ++- src/Idris/REPL.idr | 7 ++++--- src/TTImp/TTImp.idr | 3 ++- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 2146cd33f88..36acb4e6ae6 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -605,7 +605,8 @@ mutual showClause mode (WithClause fc lhs rig wval prf flags cls) -- TODO print flags = unwords [ show lhs, "with" - , showCount rig $ maybe id (\ nm => (++ " proof \{showCount (fst nm) $ show (snd nm)}")) prf + -- TODO: remove `the` after fix idris-lang/Idris2#3418 + , showCount rig $ maybe id (the (_ -> _) $ \(rg, nm) => (++ " proof \{showCount rg $ show nm}")) prf $ showParens True (show wval) , "{", joinBy "; " (assert_total $ map (showClause mode) cls), "}" ] diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index e18989f802f..1234cda893f 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -224,11 +224,12 @@ printClause l i (WithClause _ lhsraw rig wvraw prf flags csraw) = do lhs <- pterm $ map defaultKindedName lhsraw -- hack wval <- pterm $ map defaultKindedName wvraw -- hack cs <- traverse (printClause l (i + 2)) csraw - pure (relit l ((pack (replicate i ' ') + pure (relit l (pack (replicate i ' ') ++ show lhs ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")" - ++ maybe "" (\ nm => " proof " ++ showCount (fst nm) ++ show (snd nm)) prf - ++ "\n")) + -- TODO: remove `the` after fix idris-lang/Idris2#3418 + ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf + ++ "\n") ++ showSep "\n" cs) printClause l i (ImpossibleClause _ lhsraw) = do lhs <- pterm $ map defaultKindedName lhsraw -- hack diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index bed9d7ff5f4..62049eaef48 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -442,7 +442,8 @@ mutual show (WithClause fc lhs rig wval prf flags block) = show lhs ++ " with " ++ showCount rig ++ "(" ++ show wval ++ ")" - ++ maybe "" (\ nm => " proof " ++ showCount (fst nm) ++ show (snd nm)) prf + -- TODO: remove `the` after fix idris-lang/Idris2#3418 + ++ maybe "" (the (_ -> _) $ \(rg, nm) => " proof " ++ showCount rg ++ show nm) prf ++ "\n\t" ++ show block show (ImpossibleClause fc lhs) = show lhs ++ " impossible" From 3b58e1c3f75a9064c11c8e6cf33103525a1970fa Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 9 Dec 2024 14:29:26 +0300 Subject: [PATCH 4/5] [ test ] Add test for 0 proof in elaborator script --- .../with/with012/WithProof0ElabFail.idr | 34 +++++++++++++++++++ tests/idris2/with/with012/expected | 1 + tests/idris2/with/with012/run | 1 + 3 files changed, 36 insertions(+) create mode 100644 tests/idris2/with/with012/WithProof0ElabFail.idr diff --git a/tests/idris2/with/with012/WithProof0ElabFail.idr b/tests/idris2/with/with012/WithProof0ElabFail.idr new file mode 100644 index 00000000000..e882e710b58 --- /dev/null +++ b/tests/idris2/with/with012/WithProof0ElabFail.idr @@ -0,0 +1,34 @@ +module WithProof0ElabFail + +import Language.Reflection + +%default total + +%language ElabReflection + +%hide List.filter + +data So : Bool -> Type where + Oh : So True + +eqToSo : b = True -> So b +eqToSo Refl = Oh + +data All : (0 p : a -> Type) -> List a -> Type where + Nil : All p Nil + (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs) + +filter : (p : a -> Bool) -> (xs : List a) -> List a +filter p [] = [] +filter p (x :: xs) with (p x) + filter p (x :: xs) | False = filter p xs + filter p (x :: xs) | True = x :: filter p xs + +failing "While processing right hand side of with block in allFilter. prf is not accessible in this context" + %runElab declare `[ + allFilter : (p : a -> Bool) -> (xs : List a) -> All (So . p) (filter p xs) + allFilter p [] = [] + allFilter p (x :: xs) with (p x) proof 0 prf + allFilter p (x :: xs) | False = allFilter p xs + allFilter p (x :: xs) | True = eqToSo prf :: allFilter p xs + ] diff --git a/tests/idris2/with/with012/expected b/tests/idris2/with/with012/expected index c90e84658d3..5a70e8df212 100644 --- a/tests/idris2/with/with012/expected +++ b/tests/idris2/with/with012/expected @@ -2,3 +2,4 @@ 1/1: Building WithProof1 (WithProof1.idr) 1/1: Building WithProof0Fail (WithProof0Fail.idr) 1/1: Building WithProof1Fail (WithProof1Fail.idr) +1/1: Building WithProof0ElabFail (WithProof0ElabFail.idr) diff --git a/tests/idris2/with/with012/run b/tests/idris2/with/with012/run index d0852365cc0..d5c0f2b322f 100755 --- a/tests/idris2/with/with012/run +++ b/tests/idris2/with/with012/run @@ -4,3 +4,4 @@ check WithProof0.idr check WithProof1.idr check WithProof0Fail.idr check WithProof1Fail.idr +check WithProof0ElabFail.idr From afea968c2f1a0b42d58d4bdb8e4a23fd67a5b503 Mon Sep 17 00:00:00 2001 From: Viktor Yudov Date: Mon, 9 Dec 2024 15:36:51 +0300 Subject: [PATCH 5/5] [ cleanup ] Use `So` and `All` from base in tests --- tests/idris2/with/with012/WithProof0ElabFail.idr | 12 ++---------- tests/idris2/with/with012/WithProof0Fail.idr | 13 +++---------- 2 files changed, 5 insertions(+), 20 deletions(-) diff --git a/tests/idris2/with/with012/WithProof0ElabFail.idr b/tests/idris2/with/with012/WithProof0ElabFail.idr index e882e710b58..9c3f1c47fad 100644 --- a/tests/idris2/with/with012/WithProof0ElabFail.idr +++ b/tests/idris2/with/with012/WithProof0ElabFail.idr @@ -1,5 +1,7 @@ module WithProof0ElabFail +import Data.So +import Data.List.Quantifiers import Language.Reflection %default total @@ -8,16 +10,6 @@ import Language.Reflection %hide List.filter -data So : Bool -> Type where - Oh : So True - -eqToSo : b = True -> So b -eqToSo Refl = Oh - -data All : (0 p : a -> Type) -> List a -> Type where - Nil : All p Nil - (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs) - filter : (p : a -> Bool) -> (xs : List a) -> List a filter p [] = [] filter p (x :: xs) with (p x) diff --git a/tests/idris2/with/with012/WithProof0Fail.idr b/tests/idris2/with/with012/WithProof0Fail.idr index 2cac831b57e..f4178b694d0 100644 --- a/tests/idris2/with/with012/WithProof0Fail.idr +++ b/tests/idris2/with/with012/WithProof0Fail.idr @@ -1,19 +1,12 @@ module WithProof0Fail +import Data.So +import Data.List.Quantifiers + %default total %hide List.filter -data So : Bool -> Type where - Oh : So True - -eqToSo : b = True -> So b -eqToSo Refl = Oh - -data All : (0 p : a -> Type) -> List a -> Type where - Nil : All p Nil - (::) : {0 xs : List a} -> p x -> All p xs -> All p (x :: xs) - filter : (p : a -> Bool) -> (xs : List a) -> List a filter p [] = [] filter p (x :: xs) with (p x)