vituscze

Privacy Policy

Last updated: 2026-07-02

This Privacy Policy explains how the Anti-spam Bot ("the Bot") processes information while operating on Discord.

1. Information We Process

The Bot is designed solely to provide automated moderation features for Discord servers.

vituscze

firstFit(Start, Len, [], Start, [Start-Len]).
firstFit(Start, Len, [Alloc-AllocLen|Rest], Pos, NewTaken) :-
    Start + Len =< Alloc -> Pos = Start, NewTaken = [Start-Len,Alloc-AllocLen|Rest];
    NewStart is Alloc + AllocLen, firstFit(NewStart, Len, Rest, Pos, RestTaken), NewTaken = [Alloc-AllocLen|RestTaken].

merge([], []).
merge([X], [X]).
merge([A-AL, B-BL|Rest], New) :-
    B is A + AL -> L is AL + BL, merge([A-L|Rest], New);
    merge([B-BL|Rest], RestNew), New = [A-AL|RestNew].

vituscze

import Data.List
import Data.Ord

prekomprese :: String -> [(Int, Int, Char)]
prekomprese = go ""
  where
    go _  [] = []
    go ls rs = case rest of
        []    -> error "prekomprese: internal error"
        r:rest' -> (length ls - offset, len, r):go (ls ++ prefix ++ [r]) rest'

vituscze

module Classical where

open import Data.Empty
  using (⊥-elim)
open import Data.Product
  using (_×_; _,_)
open import Data.Sum
  using (_⊎_; inj₁; inj₂; [_,_])
open import Function
  using (id; _∘_)

vituscze

module Idr where

open import Function.Equality
open import Function.Inverse
open import Level
open import Relation.Binary.PropositionalEquality
  renaming (cong to cong-f)

record _≃_ {a b} (A : Set a) (B : Set b) : Set (a ⊔ b) where
  constructor iso

vituscze

module Del where

open import Data.Nat
open import Relation.Binary.Core

data List : Set where
   nil : List
   _::_ : (x : ℕ) -> (xs : List) -> List

-- membership within a list

vituscze

module Contr where

open import Data.Product
open import Data.Unit
open import Function
open import Relation.Binary.PropositionalEquality

is-contr : ∀ {a} (A : Set a) → Set _
is-contr A = Σ A λ a → ∀ x → a ≡ x

vituscze

module Norm where

open import Data.Empty
open import Data.Nat
open import Data.Product
open import Data.Sum
open import Function
open import Relation.Binary.PropositionalEquality

data Int : Set where

vituscze

open import Relation.Binary

module Data.Extended-key
  {k ℓ₁ ℓ₂}
  {Key : Set k}
  {_≈_ : Rel Key ℓ₁}
  {_<_ : Rel Key ℓ₂}
  (isStrictTotalOrder′ : IsStrictTotalOrder _≈_ _<_)
  where

vituscze

{-# OPTIONS --without-K #-}
module Incompatibility where

open import Data.Bool
open import Data.Empty
open import Data.Product
open import Data.Unit
open import Function
open import Level
open import Relation.Binary.PropositionalEquality