jespercockx

open import Data.Bool.Base
open import Data.List.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Unit

open import Function

open import Reflection
open import Reflection.TypeChecking.Monad.Syntax

jespercockx

--{-# OPTIONS -v any-auto:10 #-}

open import Data.List
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Data.List.Relation.Unary.Any.Properties using
  (singleton⁺; map⁺; mapMaybe⁺; ++⁺ˡ; ++⁺ʳ; concat⁺)
open import Data.Maybe using (Maybe; nothing; just)
open import Data.Maybe.Relation.Unary.Any using (just) renaming (Any to MAny)
open import Data.Nat using (ℕ; zero; suc; _+_)

y-taka-23

(******************************************************)
(** //// Validation of the "filter" Function ////     *)
(******************************************************)

Require Import List Bool Lt.

Section Filter.


(*////////////////////////////////////////////////////*)