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

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