Skip pattern synonyms + Warn about skipped definitions

base/Control/Applicative.v

@@ -44,6 +44,8 @@ Definition unwrapArrow {a : Type -> Type -> Type} {b} {c} (arg_0__
 
 (* Converted value declarations: *)
 
+(* Skipping definition `Control.Applicative.optional' *)
+
 (* Skipping all instances of class `GHC.Generics.Generic', including
    `Control.Applicative.Generic__WrappedMonad' *)
 

base/Control/Arrow.v

@@ -221,6 +221,8 @@ Notation "'_^>>_'" := (op_zczgzg__).
 
 Infix "^>>" := (_^>>_) (at level 99).
 
+(* Skipping definition `Control.Arrow.leftApp' *)
+
 Local Definition Arrow__arrow_arr
    : forall {b} {c}, (b -> c) -> GHC.Prim.arrow b c :=
   fun {b} {c} => fun f => f.

base/Control/Monad.v

@@ -41,6 +41,10 @@ Definition zipWithM {m} {a} {b} {c} `{_ : GHC.Base.Applicative m}
 Definition unless {f} `{(GHC.Base.Applicative f)} : bool -> f unit -> f unit :=
   fun p s => if p : bool then GHC.Base.pure tt else s.
 
+(* Skipping definition `Control.Monad.replicateM_' *)
+
+(* Skipping definition `Control.Monad.replicateM' *)
+
 Definition op_zlzdznzg__ {m} {a} {b} `{GHC.Base.Monad m}
    : (a -> b) -> m a -> m b :=
   fun f m =>
@@ -66,10 +70,16 @@ Notation "'_<=<_'" := (op_zlzezl__).
 
 Infix "<=<" := (_<=<_) (at level 99).
 
+(* Skipping definition `Control.Monad.mfilter' *)
+
 Definition mapAndUnzipM {m} {a} {b} {c} `{(GHC.Base.Applicative m)}
    : (a -> m (b * c)%type) -> list a -> m (list b * list c)%type :=
   fun f xs => GHC.List.unzip Data.Functor.<$> Data.Traversable.traverse f xs.
 
+(* Skipping definition `Control.Monad.guard' *)
+
+(* Skipping definition `Control.Monad.forever' *)
+
 Definition foldM_ {t} {m} {b} {a} `{Data.Foldable.Foldable t} `{GHC.Base.Monad
   m}
    : (b -> a -> m b) -> b -> t a -> m unit :=

base/Data/Bifoldable.v

@@ -88,6 +88,16 @@ Definition bior {t} `{Bifoldable t} : t bool bool -> bool :=
 Definition binull {t} {a} {b} `{Bifoldable t} : t a b -> bool :=
   bifoldr (fun arg_0__ arg_1__ => false) (fun arg_2__ arg_3__ => false) true.
 
+(* Skipping definition `Data.Bifoldable.bimsum' *)
+
+(* Skipping definition `Data.Bifoldable.biminimumBy' *)
+
+(* Skipping definition `Data.Bifoldable.biminimum' *)
+
+(* Skipping definition `Data.Bifoldable.bimaximumBy' *)
+
+(* Skipping definition `Data.Bifoldable.bimaximum' *)
+
 Definition bimapM_ {t} {f} {a} {c} {b} {d} `{Bifoldable t}
   `{GHC.Base.Applicative f}
    : (a -> f c) -> (b -> f d) -> t a b -> f unit :=
@@ -110,6 +120,8 @@ Definition bifoldrM {t} {m} {a} {c} {b} `{Bifoldable t} `{GHC.Base.Monad m}
     let f' := fun k x z => f x z GHC.Base.>>= k in
     bifoldl f' g' GHC.Base.return_ xs z0.
 
+(* Skipping definition `Data.Bifoldable.bifoldr1' *)
+
 Definition bifoldr' {t} {a} {c} {b} `{Bifoldable t}
    : (a -> c -> c) -> (b -> c -> c) -> c -> t a b -> c :=
   fun f g z0 xs =>
@@ -123,6 +135,8 @@ Definition bifoldlM {t} {m} {a} {b} {c} `{Bifoldable t} `{GHC.Base.Monad m}
     let f' := fun x k z => f z x GHC.Base.>>= k in
     bifoldr f' g' GHC.Base.return_ xs z0.
 
+(* Skipping definition `Data.Bifoldable.bifoldl1' *)
+
 Definition bifoldl' {t} {a} {b} {c} `{Bifoldable t}
    : (a -> b -> a) -> (a -> c -> a) -> a -> t b c -> a :=
   fun f g z0 xs =>
@@ -151,6 +165,8 @@ Definition biconcatMap {t} {a} {c} {b} `{Bifoldable t}
 Definition biconcat {t} {a} `{Bifoldable t} : t (list a) (list a) -> list a :=
   bifold.
 
+(* Skipping definition `Data.Bifoldable.biasum' *)
+
 Definition biany {t} {a} {b} `{Bifoldable t}
    : (a -> bool) -> (b -> bool) -> t a b -> bool :=
   fun p q =>

base/Data/Foldable.v

@@ -193,6 +193,12 @@ Definition elem {f} `{Foldable f} {a} `{GHC.Base.Eq_ a} : a -> f a -> bool :=
 Definition notElem {t} {a} `{Foldable t} `{GHC.Base.Eq_ a} : a -> t a -> bool :=
   fun x => negb GHC.Base.∘ elem x.
 
+(* Skipping definition `Data.Foldable.msum' *)
+
+(* Skipping definition `Data.Foldable.minimumBy' *)
+
+(* Skipping definition `Data.Foldable.maximumBy' *)
+
 Definition mapM_ {t} {m} {a} {b} `{Foldable t} `{GHC.Base.Monad m}
    : (a -> m b) -> t a -> m unit :=
   fun f => foldr (_GHC.Base.>>_ GHC.Base.∘ f) (GHC.Base.return_ tt).
@@ -288,6 +294,8 @@ Definition concat {t} {a} `{Foldable t} : t (list a) -> list a :=
     GHC.Base.build' (fun _ =>
                        fun c n => foldr (fun x y => (@foldr _ Foldable__list _ _ c y x)) n xs).
 
+(* Skipping definition `Data.Foldable.asum' *)
+
 Definition and {t} `{Foldable t} : t bool -> bool :=
   Coq.Program.Basics.compose Data.SemigroupInternal.getAll (foldMap
                               Data.SemigroupInternal.Mk_All).

base/Data/Function.v

@@ -26,6 +26,8 @@ Infix "&" := (_&_) (at level 99).
 Definition on {b} {c} {a} : (b -> b -> c) -> (a -> b) -> a -> a -> c :=
   fun lop_ziztzi__ f => fun x y => lop_ziztzi__ (f x) (f y).
 
+(* Skipping definition `Data.Function.fix_' *)
+
 Module Notations.
 Notation "'_Data.Function.&_'" := (op_za__).
 Infix "Data.Function.&" := (_&_) (at level 99).

base/Data/Functor/Classes.v

@@ -75,6 +75,54 @@ Definition liftCompare `{g__0__ : Ord1 f}
 
 (* Converted value declarations: *)
 
+(* Skipping definition `Data.Functor.Classes.showsUnaryWith' *)
+
+(* Skipping definition `Data.Functor.Classes.showsUnary1' *)
+
+(* Skipping definition `Data.Functor.Classes.showsUnary' *)
+
+(* Skipping definition `Data.Functor.Classes.showsPrec2' *)
+
+(* Skipping definition `Data.Functor.Classes.showsPrec1' *)
+
+(* Skipping definition `Data.Functor.Classes.showsBinaryWith' *)
+
+(* Skipping definition `Data.Functor.Classes.showsBinary1' *)
+
+(* Skipping definition `Data.Functor.Classes.readsUnaryWith' *)
+
+(* Skipping definition `Data.Functor.Classes.readsUnary1' *)
+
+(* Skipping definition `Data.Functor.Classes.readsUnary' *)
+
+(* Skipping definition `Data.Functor.Classes.readsPrec2' *)
+
+(* Skipping definition `Data.Functor.Classes.readsPrec1' *)
+
+(* Skipping definition `Data.Functor.Classes.readsData' *)
+
+(* Skipping definition `Data.Functor.Classes.readsBinaryWith' *)
+
+(* Skipping definition `Data.Functor.Classes.readsBinary1' *)
+
+(* Skipping definition `Data.Functor.Classes.readUnaryWith' *)
+
+(* Skipping definition `Data.Functor.Classes.readPrec2' *)
+
+(* Skipping definition `Data.Functor.Classes.readPrec1' *)
+
+(* Skipping definition `Data.Functor.Classes.readData' *)
+
+(* Skipping definition `Data.Functor.Classes.readBinaryWith' *)
+
+(* Skipping definition `Data.Functor.Classes.liftReadListPrecDefault' *)
+
+(* Skipping definition `Data.Functor.Classes.liftReadListPrec2Default' *)
+
+(* Skipping definition `Data.Functor.Classes.liftReadListDefault' *)
+
+(* Skipping definition `Data.Functor.Classes.liftReadList2Default' *)
+
 Definition eq2 {f} {a} {b} `{Eq2 f} `{GHC.Base.Eq_ a} `{GHC.Base.Eq_ b}
    : f a b -> f a b -> bool :=
   liftEq2 _GHC.Base.==_ _GHC.Base.==_.

base/Data/Functor/Utils.v

@@ -66,6 +66,8 @@ Instance Unpeel_Max {a} : Prim.Unpeel (Max a) (option a)
 
 (* Converted value declarations: *)
 
+(* Skipping definition `Data.Functor.Utils.hash_compose' *)
+
 Local Definition Semigroup__Max_op_zlzlzgzg__ {inst_a} `{GHC.Base.Ord inst_a}
    : (Max inst_a) -> (Max inst_a) -> (Max inst_a) :=
   fun arg_0__ arg_1__ =>

base/Data/List/NonEmpty.v

@@ -121,12 +121,22 @@ Definition unzip {f} {a} {b} `{GHC.Base.Functor f}
   fun xs =>
     pair (Data.Tuple.fst Data.Functor.<$> xs) (Data.Tuple.snd Data.Functor.<$> xs).
 
+(* Skipping definition `Data.List.NonEmpty.unfoldr' *)
+
+(* Skipping definition `Data.List.NonEmpty.unfold' *)
+
+(* Skipping definition `Data.List.NonEmpty.transpose' *)
+
+(* Skipping definition `Data.List.NonEmpty.toList' *)
+
 Definition takeWhile {a} : (a -> bool) -> GHC.Base.NonEmpty a -> list a :=
   fun p => GHC.List.takeWhile p GHC.Base.∘ toList.
 
 Definition take {a} : GHC.Num.Int -> GHC.Base.NonEmpty a -> list a :=
   fun n => GHC.List.take n GHC.Base.∘ toList.
 
+(* Skipping definition `Data.List.NonEmpty.tails' *)
+
 Definition tail {a} : GHC.Base.NonEmpty a -> list a :=
   fun '(GHC.Base.NEcons _ as_) => as_.
 
@@ -138,14 +148,34 @@ Definition span {a}
    : (a -> bool) -> GHC.Base.NonEmpty a -> (list a * list a)%type :=
   fun p => GHC.List.span p GHC.Base.∘ toList.
 
+(* Skipping definition `Data.List.NonEmpty.sortBy' *)
+
 Definition sortWith {o} {a} `{GHC.Base.Ord o}
    : (a -> o) -> GHC.Base.NonEmpty a -> GHC.Base.NonEmpty a :=
   sortBy GHC.Base.∘ Data.Ord.comparing.
 
+(* Skipping definition `Data.List.NonEmpty.sort' *)
+
+(* Skipping definition `Data.List.NonEmpty.some1' *)
+
+(* Skipping definition `Data.List.NonEmpty.scanr1' *)
+
+(* Skipping definition `Data.List.NonEmpty.scanr' *)
+
+(* Skipping definition `Data.List.NonEmpty.scanl1' *)
+
+(* Skipping definition `Data.List.NonEmpty.scanl' *)
+
+(* Skipping definition `Data.List.NonEmpty.reverse' *)
+
+(* Skipping definition `Data.List.NonEmpty.repeat' *)
+
 Definition partition {a}
    : (a -> bool) -> GHC.Base.NonEmpty a -> (list a * list a)%type :=
   fun p => Data.OldList.partition p GHC.Base.∘ toList.
 
+(* Skipping definition `Data.List.NonEmpty.op_znzn__' *)
+
 Definition op_zlzb__ {a} : a -> GHC.Base.NonEmpty a -> GHC.Base.NonEmpty a :=
   fun arg_0__ arg_1__ =>
     match arg_0__, arg_1__ with
@@ -187,9 +217,15 @@ Definition map {a} {b}
     | f, GHC.Base.NEcons a as_ => GHC.Base.NEcons (f a) (GHC.Base.fmap f as_)
     end.
 
+(* Skipping definition `Data.List.NonEmpty.lift' *)
+
 Definition length {a} : GHC.Base.NonEmpty a -> GHC.Num.Int :=
   fun '(GHC.Base.NEcons _ xs) => #1 GHC.Num.+ Data.Foldable.length xs.
 
+(* Skipping definition `Data.List.NonEmpty.last' *)
+
+(* Skipping definition `Data.List.NonEmpty.iterate' *)
+
 Definition isPrefixOf {a} `{GHC.Base.Eq_ a}
    : list a -> GHC.Base.NonEmpty a -> bool :=
   fun arg_0__ arg_1__ =>
@@ -199,9 +235,35 @@ Definition isPrefixOf {a} `{GHC.Base.Eq_ a}
         andb (y GHC.Base.== x) (Data.OldList.isPrefixOf ys xs)
     end.
 
+(* Skipping definition `Data.List.NonEmpty.intersperse' *)
+
+(* Skipping definition `Data.List.NonEmpty.insert' *)
+
+(* Skipping definition `Data.List.NonEmpty.inits' *)
+
+(* Skipping definition `Data.List.NonEmpty.init' *)
+
 Definition head {a} : GHC.Base.NonEmpty a -> a :=
   fun '(GHC.Base.NEcons a _) => a.
 
+(* Skipping definition `Data.List.NonEmpty.groupWith1' *)
+
+(* Skipping definition `Data.List.NonEmpty.groupWith' *)
+
+(* Skipping definition `Data.List.NonEmpty.groupBy1' *)
+
+(* Skipping definition `Data.List.NonEmpty.groupBy' *)
+
+(* Skipping definition `Data.List.NonEmpty.groupAllWith1' *)
+
+(* Skipping definition `Data.List.NonEmpty.groupAllWith' *)
+
+(* Skipping definition `Data.List.NonEmpty.group1' *)
+
+(* Skipping definition `Data.List.NonEmpty.group' *)
+
+(* Skipping definition `Data.List.NonEmpty.fromList' *)
+
 Definition filter {a} : (a -> bool) -> GHC.Base.NonEmpty a -> list a :=
   fun p => GHC.List.filter p GHC.Base.∘ toList.
 
@@ -211,6 +273,8 @@ Definition dropWhile {a} : (a -> bool) -> GHC.Base.NonEmpty a -> list a :=
 Definition drop {a} : GHC.Num.Int -> GHC.Base.NonEmpty a -> list a :=
   fun n => GHC.List.drop n GHC.Base.∘ toList.
 
+(* Skipping definition `Data.List.NonEmpty.cycle' *)
+
 Definition cons_ {a} : a -> GHC.Base.NonEmpty a -> GHC.Base.NonEmpty a :=
   _<|_.
 

base/Data/Maybe.v

@@ -61,6 +61,8 @@ Definition isJust {a} : option a -> bool :=
 Definition fromMaybe {a} : a -> option a -> a :=
   fun d x => match x with | None => d | Some v => v end.
 
+(* Skipping definition `Data.Maybe.fromJust' *)
+
 Definition catMaybes {a} : list (option a) -> list a :=
   fun ls =>
     let cont_0__ arg_1__ :=