bigs

const CHUNK_SIZE = 50;

class FetchUsers implements AsyncIterable<string> {
  #users: string[]; 
  #chunk: number;

  constructor() {
    this.#chunk = 0;
    this.#users = [];
  }

bigs

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

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

module FFIExample

import System.FFI

-- System info helpers

export
%foreign "C:int_size_bytes,shim"
prim_int_size_bytes : Int

bigs

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

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

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

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

#!/bin/bash ruby

require "open3"

sigint_caught = false
Signal.trap("INT") do
  sigint_caught = true
  throw :sigint
end

bigs

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: