This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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[] = []> = |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
class Maybe { | |
constructor(isJust, value) { | |
this.isJust = isJust | |
if (isJust) { | |
this.value = value | |
} | |
} | |
static just(value) { | |
return new Maybe(true, value) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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() } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |> |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Main | |
import Data.Vect | |
infixr 5 .+. | |
data Schema | |
= SString | |
| SChar | |
| SInt |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module NamelessLambda | |
%default total | |
%access public export | |
data Term: Type where | |
Var : Nat -> Term | |
Lambda : Term -> Term | |
Apply : Term -> Term -> Term |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Term | |
%default total | |
data Term : Type where | |
Zero : Term | |
True : Term | |
False : Term | |
Succ : Term -> Term | |
Pred : Term -> Term |
NewerOlder