clayrat

object FooSchema extends DeserializationSchema[Foo] {
  def getProducedType = createTypeInformation[Foo]
  def isEndOfStream(nextElement: Foo) = false
  def deserialize(message: Array[Byte]) = Foo.parseFrom(message)
}

clayrat

package j;

public interface Bar {
}

clayrat

package ca

import scalaz.{Comonad, NonEmptyList, Zipper}
import Zipper._

case class Board[A](p: Zipper[Zipper[A]]) {
  def up = Board(p.previous.get)
  def down = Board(p.next.get)
  def left = Board(p.map(_.previous.get))
  def right = Board(p.map(_.next.get))

clayrat

leLtOrEq : (x, y : Bin) -> x `Le` y -> Either (x `Lt` y) (x=y)
leLtOrEq x y xley with (x `compare` y) proof xy
  | LT = Left Refl
  | EQ = Right $ compareEqIffTo x y (sym xy)
  | GT = absurd $ xley Refl

ltTrans : (p, q, r : Bin) -> p `Lt` q -> q `Lt` r -> p `Lt` r
ltTrans p q r = 
  peanoRect 
    (\x => (s, t : Bin) -> s `Lt` t -> t `Lt` x -> s `Lt` x)

clayrat

decAnd : Dec a -> Dec b -> Dec (a,b)
decAnd (Yes a) (Yes b) = Yes (a, b)
decAnd  _      (No nb) = No (nb . snd)
decAnd (No na)  _      = No (na . fst)

decOr : Dec a -> Dec b -> Dec (Either a b)
decOr (Yes a)  _      = Yes (Left a)
decOr  _      (Yes b) = Yes (Right b)
decOr (No na) (No nb) = No (either na nb) 

clayrat

import Control.Isomorphism
import Control.Category

funext : {a,b : Type} -> {f, g : a -> b} -> ((x : a) -> f x = g x) -> f = g
funext fxgx = really_believe_me fxgx 

isoCurry : Iso (a->b->c) ((a,b)->c)
isoCurry =
  MkIso
    uncurry

clayrat

module Qsort

%default total

data PreOrder : (a : Type) -> (a -> a -> Type) -> Type where
  PrO : {ltef : a -> a -> Type} -- <=
      -> ((x, y, z : a) -> ltef x y -> ltef y z -> ltef x z)  -- transitivity
      -> PreOrder a ltef

data TotalOrder : (a : Type) -> (a -> a -> Type) -> Type where

clayrat

module GradedMonad

import Data.Vect

%default total
%access public export

interface GMonad (g : k -> Type -> Type) where
  Zero : k
  Plus : k -> k -> k

clayrat

module FSMCat

import Control.Category
import Data.Morphisms
import Data.Vect
import Interfaces.Verified

%access public export
%default total

clayrat

def connection/quad (A : type) 
    (abx : 𝕀 → A) 
    (aby : [k] A [k=0 → abx 0 | k=1 → abx 1]) 
    (bax : [k] A [k=0 → abx 1 | k=1 → abx 0]) 
    (bay : [k] A [k=0 → abx 1 | k=1 → abx 0]) 
    (abxy : path (𝕀 → A) abx aby)
    (baxy : path (𝕀 → A) bax bay)
  : [i j] A [
    | i=0 → aby j 
    | i=1 → bay j