chryslovelace

// compile with `gcc -shared -o tuesday.so tuesday.c`

#include <time.h>

int day_of_week()
{
    time_t t;
    time(&t);
    return localtime(&t)->tm_wday;
}

chryslovelace

module nono

import Data.Vect

mutual
    data Descriptor : Nat -> Type where
        Nil : Descriptor n
        (::) : (k : Nat) -> (d : Descriptor n) -> Descriptor (k + n + isNotEmpty d)

    isNotEmpty : Descriptor n -> Nat

chryslovelace

module sess

import System.Concurrency.Channels

infix 3 :!:, :?:
infix 2 :+:, :&:

data Protocol : Type where
    Eps : Protocol
    (:!:) : Type -> Protocol -> Protocol