idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 12:42:02 +03:00
Code Issues Projects Releases Wiki Activity

Remove my debugging noise from test case

Browse Source
This commit is contained in:
Edwin Brady 2020-07-01 00:43:33 +01:00
parent 25491060e2
commit 669e50ff55
1 changed files with 1 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
tests/idris2/reg029/lqueue.idr
View File

@ -9,10 +9,6 @@ data CatList : (Type -> Type) -> Type -> Type where
E : CatList q a
C : {0 q : Type -> Type} -> a -> q (Lazy (CatList q a)) -> CatList q a
-- %logging 5
partial
link : (Queue q) => CatList q a -> Lazy (CatList q a) -> CatList q a
link E s = s -- Just to satisfy totality for now.
link (C x xs) s = C x (snoc xs s) -- can't solve constraint between
-- Lazy (CatList q a) and CatList q a
-- %logging 0
link (C x xs) s = C x (snoc xs s)