GallagherCommaJack

import torch
import torch.nn.functional as F
from einops import reduce, rearrange

class DepthwiseRematConvFn(torch.autograd.Function):
    @staticmethod
    def forward(
        ctx,
        input,
        k1,

GallagherCommaJack

class CrossAttentionModConv2d(nn.Module):
    def __init__(self, state, ch, d_context, ch_q=None, d_v=None, n_head=1):
        super().__init__()
        assert ch % n_head == 0
        self.state = state
        self.n_head = n_head
        self.ch = ch
        self.d_context = d_context
        self.ch_q = ch_q or self.ch
        self.d_v = d_v or self.d_context

GallagherCommaJack

from math import sqrt

import torch
from fast_transformers.attention_registry import (
    AttentionRegistry, EventDispatcherInstance, Float, Optional,
    RecurrentAttentionRegistry, RecurrentCrossAttentionRegistry)
from fast_transformers.builders import (RecurrentDecoderBuilder,
                                        RecurrentEncoderBuilder,
                                        TransformerDecoderBuilder,
                                        TransformerEncoderBuilder)

GallagherCommaJack

import torch
import torch.nn as nn
import torch.nn.functional as TF
import torch.utils.data as D
import torchvision as Tv

import pytorch_lightning as pl

def init_weights(m):
    if type(m) == nn.Conv2d or type(m) == nn.ConvTranspose2d:

GallagherCommaJack

Keybase proof

I hereby claim:

• I am gallaghercommajack on github.
• I am theseriousadult (https://keybase.io/theseriousadult) on keybase.
• I have a public key ASBBkJegFu_s7UqQ-UN1m1Ji8NHDz6fZeJI6bW0L1lERlgo

To claim this, I am signing this object:

GallagherCommaJack

data Ty : Set
data Tm : Ty → Set

postulate Var : Ty → Set

data Ty where
  pi sg : (A : Ty)(B : Var A → Ty) → Ty

data Subst {A} : (Var A → Ty) → Tm A → Ty → Set where
  -- need to fill this in

GallagherCommaJack

dashSlashSlashDelete :: (Show a, Show b, Show c) => a -> b -> c -> Routes
dashSlashSlashDelete a b c = let sa = show a
                                 sb = if length (show b) < 2 then '0':show b else show b
                                 sc = if length (show c) < 2 then '0':show c else show c
                             in gsubRoute (fold $ intersperse "-" [sa, sb, sc, ""]) (const $ fold $ intersperse "/" [sa, sb, ""])  -- gsubRoute apparently succeeds even when it should fail
                                `composeRoutes` matchRoute (fromGlob "*/*/*") idRoute -- this oughta fix that


dashSlashList :: (Show a, Show b, Show c) => [a] -> [b] -> [c] -> [Routes]
dashSlashList as bs cs = [dashSlashSlashDelete a b c | a <- as, b <- bs, c <- cs]

GallagherCommaJack

{-# OPTIONS --without-K #-}
module mini-lob where
open import Agda.Primitive public
  using    (Level; _⊔_; lzero; lsuc)
open import Data.Unit
open import Data.Product
open import Level
infixl 2 _▻_
infixl 3 _‘’_
infixr 1 _‘→’_

GallagherCommaJack

data Context : ℕ → Set
data _+c_ {n : ℕ} (Γ : Context n) : ℕ → Set
data Type : ∀ {n} → Context n → Set
data Term : ∀ {n} (Γ : Context n) → Type Γ → Set

_++_ : ∀ {n m} (Γ : Context n) → Γ +c m → Context (m + n)
_cw_ : ∀ {x n m} {Γ : Context x} (Δ : Γ +c n) → Γ +c m → (Γ ++ Δ) +c m

data Context where
  ε₀ : Context 0

GallagherCommaJack

module well-typed-syntax where
open import Data.Nat
infixl 2 _▻_
infixl 2 _▻Type_
infixl 3 _‘’_

mutual
  data Context : ℕ → Set where
    ε₀ : Context 0
    _▻_ : ∀ {n} (Γ : Context n) → Type Γ → Context (suc n)