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:
import torch | |
import torch.nn.functional as F | |
from einops import reduce, rearrange | |
class DepthwiseRematConvFn(torch.autograd.Function): | |
@staticmethod | |
def forward( | |
ctx, | |
input, | |
k1, |
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 |
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) |
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: |
I hereby claim:
To claim this, I am signing this object:
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 |
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] |
{-# 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 _‘→’_ |
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 |
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) |