Skip to content

Instantly share code, notes, and snippets.

View bigs's full-sized avatar

bigs

58 followers · 20 following
  • Kiosk
  • Brooklyn, NY
  • 17:12 (UTC -05:00)
View GitHub Profile
@bigs
bigs / async_iterator.ts
Created April 12, 2023 20:23
const CHUNK_SIZE = 50;
class FetchUsers implements AsyncIterable<string> {
#users: string[];
#chunk: number;
constructor() {
this.#chunk = 0;
this.#users = [];
}
@bigs
bigs / antehandler.patch
Created April 26, 2022 19:26
A quick attempt at an `AnteHandler` based approach to enforcing code size limits based on a param
diff --git a/x/wasm/alias.go b/x/wasm/alias.go
index 610ce97..3e32935 100644
--- a/x/wasm/alias.go
+++ b/x/wasm/alias.go
@@ -17,7 +17,6 @@ const (
TStoreKey = types.TStoreKey
QuerierRoute = types.QuerierRoute
RouterKey = types.RouterKey
- MaxWasmSize = types.MaxWasmSize
MaxLabelSize = types.MaxLabelSize
@bigs
bigs / Arity.idr
Created August 27, 2020 14:32
Idris implementation of nmap from https://www.seas.upenn.edu/~sweirich/papers/aritygen.pdf
module Arity
import Data.Vect
export
repeat : {n : Nat} -> a -> Vect n a
repeat {n = 0} _ = []
repeat {n = S n} x = x :: repeat {n} x
export
@bigs
bigs / FFIExample.idr
Last active August 19, 2020 22:38
module FFIExample
import System.FFI
-- System info helpers
export
%foreign "C:int_size_bytes,shim"
prim_int_size_bytes : Int
@bigs
bigs / Git.idr
Last active August 18, 2020 19:33
module Libgit.Git
import Control.Monad.Reader
||| An abstract token representing the initialized libgit2 state. Its
||| constructor is purposefully not exported, a context can only be created
||| via `runGitT`.
export
data GitContext : (i : Type) -> Type where
MkGitContext : GitContext i
@bigs
bigs / Adder.idr
Created August 16, 2020 16:56
module Adder
AdderType : Nat -> Type
AdderType 0 = Int
AdderType (S k) = Int -> AdderType k
adder : {n : Nat} -> {default 0 acc : Int} -> AdderType n
adder {n=Z} {acc} = acc
adder {n=S k} {acc} = \x => adder {n=k} {acc=acc + x}
@bigs
bigs / IndexedTypes.idr
Created August 13, 2020 20:36
module IndexedTypes
data Foo i = MkFoo
data FooInt i = MkFooInt Integer
mkFooInt : Foo i -> Integer -> FooInt i
mkFooInt _ = MkFooInt
addFoos : Foo i -> FooInt i -> FooInt i -> FooInt i
addFoos f (MkFooInt x) (MkFooInt y) = mkFooInt f (x + y)
@bigs
bigs / Matrix.idr
Created August 13, 2020 04:59
module Data.Matrix
Matrix : (m: Nat) -> (n: Nat) -> (a: Type) -> Type
Matrix m n a = Vect m (Vect n a)
madd : Num a => {n : _} -> Matrix m n a -> Matrix m n a -> Matrix m n a
madd [] [] = []
madd (x :: xs) (y :: ys) = vadd {n=n} x y :: madd xs ys
where
vadd : {n : _} -> Vect n a -> Vect n a -> Vect n a
@bigs
bigs / git-hatchet
Created July 21, 2020 16:03
git hatchet -- excise old branches
#!/bin/bash ruby
require "open3"
sigint_caught = false
Signal.trap("INT") do
sigint_caught = true
throw :sigint
end
@bigs
bigs / keybase.md
Created February 6, 2019 20:16

Keybase proof

I hereby claim:

  • I am bigs on github.
  • I am protocole (https://keybase.io/protocole) on keybase.
  • I have a public key ASB8fxzU6Sz1-uRaVvmHK0fR7Xt3WdowS5XXJ4HcZ4mqLQo

To claim this, I am signing this object: