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:
const CHUNK_SIZE = 50; | |
class FetchUsers implements AsyncIterable<string> { | |
#users: string[]; | |
#chunk: number; | |
constructor() { | |
this.#chunk = 0; | |
this.#users = []; | |
} |
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 |
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 |
module FFIExample | |
import System.FFI | |
-- System info helpers | |
export | |
%foreign "C:int_size_bytes,shim" | |
prim_int_size_bytes : Int |
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 |
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} |
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) |
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 |
#!/bin/bash ruby | |
require "open3" | |
sigint_caught = false | |
Signal.trap("INT") do | |
sigint_caught = true | |
throw :sigint | |
end |
I hereby claim:
To claim this, I am signing this object: