vituscze

% recodex: revize

person(O) :- member(O, [david, thomas, emma, stella]).

across(david, thomas).
across(thomas, david).
across(emma, stella).
across(stella, emma).

distinct(A, B, C, D) :-

vituscze

natural(0).
natural(s(N)) :- natural(N).

smaller(0, s(_)).
smaller(s(M), s(N)) :- smaller(M, N).

% Predikat postupne generuje dvojice prirozenych cisel X, Y tak,
% ze X < Y.
gen_smaller(X, Y) :- natural(Y), smaller(X, Y).

vituscze

zena(vdova).
zena(dcera).

muz(ja).
muz(otec).
muz(syn).
muz(otcuvSyn).

bioRodic(vdova, dcera).
bioRodic(otec, ja).

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