SekiT

type Step<Input extends string, Program extends string[]> =
  Program extends [infer ProgramHead extends string, ...infer ProgramTail]
    ? Input extends `0${infer Rest}`
      ? [Rest, [...ProgramTail, ProgramHead]]
      : Input extends `1${infer Rest}`
        ? [`${Rest}${ProgramHead}`, [...ProgramTail, ProgramHead]]
        : [Input, Program]
    : [Input, []];

type StepN<Input extends string, Program extends string[], N extends number, Counter extends 0[] = []> =

SekiT

import Data.Vect

infixl 1 =>=

interface Functor w => Comonad (w : Type -> Type) where
  extract : w a -> a

  (=>=) : (w a -> b) -> (w b -> c) -> (w a -> c)
  f =>= g = g . extend f

SekiT

function*cts(S,d){for(i=0;d;d=d.slice(1)+['',S[i++%S.length]][d[0]])yield d}

// Example usage
let j=0; for(v of cts(["01", "10"], "11")){ console.log(v); if(++j>=10) break }

SekiT

class Maybe {
  constructor(isJust, value) {
    this.isJust = isJust
    if (isJust) {
      this.value = value
    }
  }

  static just(value) {
    return new Maybe(true, value)

SekiT

const genIterator = (iterable) =>
  typeof iterable === 'function' ? iterable() : iterable[Symbol.iterator]()

class Stream {
  constructor(iterable = []) {
    this._iterable = iterable
    this._iterator = genIterator(iterable)
  }

  next() { return this._iterator.next() }

SekiT

import ZZ

%default total

integralDomainN : Not (m = Z) -> Not (n = Z) -> Not (m * n = Z)
integralDomainN mNotZ nNotZ mnEqZ {m = Z} = mNotZ Refl
integralDomainN mNotZ nNotZ mnEqZ {n = Z} = nNotZ Refl
integralDomainN mNotZ nNotZ mnEqZ {m = S a} {n = S b} = uninhabited mnEqZ

infixl 9 |>

SekiT

module ZZ

import Data.Sign

%default total
%access public export

data Diff : Nat -> Nat -> Type where
  LTByS : (d : Nat) -> Diff n (n + S d)
  GTByS : (d : Nat) -> Diff (n + S d) n

SekiT

module Main

import Data.Vect

infixr 5 .+.

data Schema
  = SString
  | SChar
  | SInt

SekiT

module NamelessLambda

%default total
%access public export

data Term: Type where
  Var    : Nat -> Term
  Lambda : Term -> Term
  Apply  : Term -> Term -> Term

SekiT

module Term

%default total

data Term : Type where
  Zero   : Term
  True   : Term
  False  : Term
  Succ   : Term -> Term
  Pred   : Term -> Term