Skip to content

Instantly share code, notes, and snippets.


mniip mniip

View GitHub Profile
View dependent_sort.v
(* Free category on a quiver *)
Inductive Free {ob} (Q : ob -> ob -> Type) : ob -> ob -> Type :=
| Id : forall {X}, Free Q X X
| Circ : forall {X Y Z}, Q Y Z -> Free Q X Y -> Free Q X Z.
Arguments Id {_ _ _}.
Arguments Circ {_ _ _ _ _}.
Fixpoint append {ob} {Q : ob -> ob -> Type} {X Y Z} (xs : Free Q Y Z) (ys : Free Q X Y)
: Free Q X Z
:= match xs, ys with
# Add rudimentary thread support into 1.7.3.
# Not intended as a permanent solution. The module must be loaded before discord is loaded anywhere in the program.
# Allows sending and receiving messages in threads, receiving thread update events.
# Administering threads doesn't work. Editing channel permission overwrites doesn't work.
# Plan:
# - Copy Thread, ThreadMember data classes from 2.0
# - Patch Guild to have threads
# - Patch ConnectionState to parse thread related gateway events
View freenode-resignation.txt
Hash: SHA256
Good evening freenode.
This is not a draft.
import asyncio
import collections
class Var:
__slots__ = "value", "lock", "version", "subscribers"
def __init__(self, value=None):
self.value = value
self.lock = asyncio.Lock()
self.version = 0
self.subscribers = set()
View DeRham.hs
This program generates a poly-line approximation to a De Rham curve. The curve
is specified using a collection of affine contractions. Under the assumption
that all fixed points are in the unit circle, the program is able to guarantee
an upper bound on the deviation of the actual curve from the poly-line
The output is a series of lines with three columns each: the value of the
parameter in [0, 1], the real part, and the imaginary part of the curve.
View UnionFind.hs
{-# LANGUAGE BangPatterns, RoleAnnotations, LambdaCase, ViewPatterns #-}
import Control.Monad
import Control.Monad.ST
import Control.Monad.ST.Unsafe
import Data.STRef
import Debug.Trace
import GHC.IO
newtype Cell s a = Cell (STRef s a)
View cd.v
Inductive opt {A : Type} : bool -> Type :=
| Nothing : opt false
| Just : A -> opt true.
Arguments opt : clear implicits.
Definition mkOpt {A : Type} {b : bool} (x : A) : opt A b :=
if b return opt A b then Just x else Nothing.
Definition mapOpt {A B : Type} {b : bool} (h : A -> B) (o : opt A b) : opt B b :=
match o with
View TF.hs
type family KnownBools (bs :: [Bool]) :: Constraint where
KnownBools '[] = ()
KnownBools (b ': bs) = (KnownBool b, KnownBools bs)
type family KnownBools (bs :: [Bool]) :: Constraint where
KnownBools '[] = ()
KnownBools '[b1] = (KnownBool b1)
KnownBools '[b1, b2] = (KnownBool b1, KnownBool b2)
KnownBools '[b1, b2, b3] = (KnownBool b1, KnownBool b2, KnownBool b3)
KnownBools (b1 ': b2 ': b3 ': b4 ': bs) = (KnownBool b1, KnownBool b2, KnownBool b3, KnownBool b4, KnownBools bs)
View kbdtop.c
#include <stdio.h>
#include <stdlib.h>
#include <stdint.h>
#include <string.h>
#include <errno.h>
#include <unistd.h>
#include <fcntl.h>
#include <sys/ioctl.h>
#include <linux/hidraw.h>
View MLens.hs
type MLens m s t a b = forall f. Traversable f => (a -> Compose m f b) -> s -> Compose m f t
mlens :: Monad m => (s -> m a) -> (s -> b -> m t) -> MLens m s t a b
mlens get set h s = Compose $ get s >>= getCompose . h >>= traverse (set s)
type MGetting m r s a = (a -> Compose m (Const r) a) -> s -> Compose m (Const r) s
mview :: Applicative m => MGetting m a s a -> s -> m a
mview l s = fmap getConst . getCompose $ l (\a -> Compose (pure (Const a))) s