nicball

with import <nixpkgs> {};

let

# type monad = {
#   type m a
#   map : (a -> b) -> m a -> m b
#   apply : m (a -> b) -> m a -> m b
#   pure : a -> m a
#   bind : m a -> (a -> m b) -> m b

nicball

with import <nixpkgs> {};

let

  # class : super -> self -> obj

  # fix : class -> obj
  fix = c: let self = c {} self; in self;

  # mix : class -> class -> class

nicball

open import Data.Nat using (ℕ ; zero ; suc) -- ; _≤_; z≤n ; s≤s ; _≤?_)
open import Data.Product using (∃-syntax) renaming (_,_ to ⟨_,_⟩)
-- open import Relation.Nullary using (Dec ; yes ; no)
-- open import Relation.Nullary.Decidable using (True ; toWitness)
-- open import Function using (id ; _∘_)
-- open import Data.List using (List ; [] ; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
-- Dependently typed lambda calculus with de Bruijn indexes

infix 19 _∋_⦂_

nicball

open import Data.Nat using (ℕ ; zero ; suc ; _≤_; z≤n ; s≤s ; _≤?_)
open import Relation.Nullary using (Dec ; yes ; no)
open import Relation.Nullary.Decidable using (True ; toWitness)
open import Function using (id ; _∘_)
open import Data.List using (List ; [] ; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)

infix 25 #ᵗ_
infix 25 #ᶠ_
infix 24 ¬_

nicball

open import Agda.Builtin.Int using (Int; pos)
open import Data.Bool using (T)
open import Data.Fin using (Fin; zero; suc)
open import Data.Nat using (ℕ)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Data.Vec using (Vec; []; _∷_; _[_]=_; here; there; _++_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary.Decidable using (True; isYes)
open import Relation.Nullary using (Dec; yes; no)

nicball

{ stdenv, lib, fetchurl, unzip, mono, makeWrapper }:

stdenv.mkDerivation rec {
  pname = "terraria-server";
  version = "1.4.3.2";
  urlVersion = lib.replaceChars [ "." ] [ "" ] version;

  src = fetchurl {
    url = "https://terraria.org/api/download/pc-dedicated-server/terraria-server-${urlVersion}.zip";
    sha256 = "sha256-/OClQTO9iBRQk3iTvYbjG1cCicKIBh+yi2OFpurJx8U=";

nicball

### Keybase proof

I hereby claim:

  * I am nicball on github.
  * I am nicball (https://keybase.io/nicball) on keybase.
  * I have a public key whose fingerprint is F917 6C67 E5E7 0914 7F6F  A3F4 A2D9 A42A 937F B5D4

To claim this, I am signing this object:

nicball

let rec remove_nth n = function
    | x :: xs ->
        if n = 0
        then xs
        else x :: remove_nth (n - 1) xs
    | [] -> raise (Failure "remove_nth");;

let rec arrange = function
    | [] -> [[]]
    | list ->

nicball

<title>学管</title>

nicball

Coro.java:39: error: method bind in class State<S#2,T#2> cannot be applied to given types;
        return new Coro<>(k -> s.bind(k));
                                ^
  required: Function<T#1,State<S#1,U>>
  found: Function<T#1,State<Queue<Coro<R,Unit>>,R>>
  reason: cannot infer type-variable(s) U
    (argument mismatch; Function<T#1,State<Queue<Coro<R,Unit>>,R>> cannot be converted to Function<T#1,State<S#1,U>>)
  where T#1,R,S#1,U,T#2,S#2 are type-variables:
    T#1 extends Object declared in method <R,T#1,S#1>liftState(State<S#1,T#1>)
    R extends Object declared in method <R,T#1,S#1>liftState(State<S#1,T#1>)