vituscze

module TicTacToe where

open import Data.Bool
  using (Bool; true; false; _∧_; _∨_)
open import Data.Empty
  using (⊥-elim)
open import Data.Fin
  using (Fin; zero; suc)
open import Data.Maybe
  using (Maybe; just; nothing)

vituscze

module AVLMembership where

open import Data.Empty
open import Data.Product
open import Level
open import Relation.Binary
open import Relation.Binary.PropositionalEquality as P using (_≡_)
open import Relation.Nullary

import Data.AVL

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

vituscze

open import Relation.Binary

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

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

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 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 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 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

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'