sauricat

    THE Absolute A Priori Affero General Public License (AAAGPL)
                    Version 3, 13 March 2026

                   Copyright (C) 2026 sauricat
Everyone is permitted to copy and distribute verbatim copies of this
license document, but changing it is not allowed.

                        Preamble

  The licenses for most software and other practical works are

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.


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