mniip

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Require Import Coq.Relations.Relations.
Require Import Coq.Compat.AdmitAxiom.

Import ListNotations.
Infix "<$>" := map (at level 65, left associativity).
Notation "k >>= f" := (flat_map f k) (at level 66, left associativity).

Definition allb {A} (f : A -> bool) (xs : list A) : bool :=

mniip

{-# LANGUAGE RankNTypes, GADTs #-}

import Data.Void

newtype Maybe' a = Maybe { unMaybe :: forall r. r -> (a -> r) -> r }

v0 :: LC (Maybe' a)
v0 = var nothing
v1 :: LC (Maybe' (Maybe' a))
v1 = var $ just nothing

mniip

(* 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

mniip

# Add rudimentary thread support into discord.py 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

mniip

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256

https://mniip.com/freenode.txt
https://gist.github.com/mniip/ae2db79154fd39af15f24687a2421498

Good evening freenode.

This is not a draft.

mniip

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()

mniip

{-
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
approximation.

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.

mniip

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

mniip

{-# 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)

mniip

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)