Skip to content

Instantly share code, notes, and snippets.

View witt3rd's full-sized avatar
⌨️
coding

Donald Thompson witt3rd

⌨️
coding
View GitHub Profile
data Foo a = Bar a
| Baz (Foo a) (Foo a)
fooEq : DecEq a => a -> a -> Foo a -> Foo a -> Maybe (Foo a)
fooEq x y f g = case decEq x y of
Yes _ => Just (Baz f g)
No _ => Nothing
comb : DecEq a => Foo a -> Foo a -> Maybe (Foo a)
comb f@(Bar x ) g@(Bar y ) = fooEq x y f g -- < ok
@witt3rd
witt3rd / zed.md
Last active October 8, 2020 13:40
Z notation

Z Notation (zed)

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{zed-csp}
\usepackage{amsthm}

\theoremstyle{definition}
@witt3rd
witt3rd / idris_cookbook.md
Last active October 8, 2020 10:16
Idris code snippets

Idris Cookbook

From Haskell

newtype

newtype WorldM a = WorldM { asT :: WorldT a }
data Foo : (x : List a) -> (y : List b) -> Type where
MkFoo : (bar: a -> b) -> Foo x y
bar : Foo {a} {b} x y -> a -> b
bar (MkFoo _) x' = ?rhs
{-
b : Type
a : Type
y : List b
record Foo where
constructor MkFoo
from : Type
to : Type
bar : (a : Foo) -> (x : from a) -> (to a)
-- impl not important
baz : (a : Foo) -> (b : Foo) -> ((to b) = (from a)) => (x: from b) -> (to a)
@witt3rd
witt3rd / random_double.idr
Created September 30, 2020 08:30
Random Double from Haskell in Idris
module RandomDouble
import Data.Bits
import Data.Vect
import Effects
import Effect.StdIO
import Effect.Random
-- 2^53 as an Integer
twoTo53 : Integer
@witt3rd
witt3rd / github.md
Last active September 24, 2020 20:13
Tips and commands for using Git and Github

Git and Github

Git

Listing the files in a commit

git diff-tree --no-commit-id --name-only -r 289b092d

Clearing Git History

@witt3rd
witt3rd / nix.md
Last active September 17, 2020 18:20
adventures in nix

nix

Install

macOS

Follow the recommended approach to prepare for the standard Linux install (below).

Linux / WSL

@witt3rd
witt3rd / haskell.md
Last active September 13, 2020 16:39
Haskell setup
@witt3rd
witt3rd / useful-q-lambdas.md
Last active September 13, 2020 16:05
Useful Q Lambdas

GraphQL requests to CKG services

// wrap in async function
return (async () => {
  // request graphql
  const data = await input.__requestCkg({
    svcRef: "/service/donald-hello-world",
    query: "query { allFoos { id } }"
  })