mathink

(* Monad with Coercion *)

Definition relation (A: Type) := A -> A -> Prop.
Hint Unfold relation.

Reserved Notation "x == y" (at level 85, no associativity).
Class Equivalence (A: Type) :=
  {
    equiv_eq: relation A where "x == y" := (equiv_eq x y);
    equiv_refl:

pasberth

• Underfly series

  • Undersky (2400年頃)
  • Underspace (2600年頃)

• Interspace series

  • Interspace (2400年〜2600年頃。人類の第2の惑星 Cold Earth への到達へ大きな役割を果たした)
  • Intersperse
  • Interspecies (4000年頃)

• Transray series

mathink

Definition relation (A: Type) := A -> A -> Prop.

(* Definition: Equivalence relation *)
Reserved Notation "x == y" (at level 80, no associativity).

Class Equivalence {A: Type}(eq: relation A) :=
  {
    equiv_eq := eq
      where "x == y" := (equiv_eq x y);

pirapira

Require Import ssreflect ssrbool eqtype ssrnat seq ssrfun fintype.

Ltac 破 := case.
Ltac 解 := elim.
Ltac 動 := move.
Ltac 割 := split.
Ltac 矣 := done.
Ltac 用 := apply.
Ltac 在 := exists.

pasberth

class T t where
  t :: t a

instance T X where
  t = tx

instance T Y where
 t = ty

masakielastic

すぐれた PHP ライブラリとリソース

Awesome PHP の記事をフォークして翻訳したものです (2013年4月25日)。おどろくほどすごい PHP ライブラリ、リソースやちょっとした情報のリストです。

【訳者コメント】 PHP 入門者のかたにはクィックリファレンスとして PHP: The Right Way 、セキュリティに関しては2011年3月に出版された 体系的に学ぶ 安全なWebアプリケーションの作り方 をおすすめします。

Composer

• Composer/Packagist - パッケージと依存マネージャー
• Composer Installers - マルチフレームワーク Composer ライブラリインストーラー。

ympbyc

[ :map ([a] (a -- b) -- [b])
   [ over
     [ [] ]
     [ swap dup car rot tuck call swap rot cdr swap map swap drop swap drop swap cons ]
     rot
     empty? ] define,

   [ 1 2 3 4 5 ] [ 2 * ] map . ]

fumieval

import Control.Applicative
import Data.Word
import System.Environment
import Text.Trifecta
import Control.Monad
import qualified Data.ByteString as BS
import qualified Data.ByteString.Lazy as BL
import qualified Codec.Binary.UTF8.String as UTF8

infixl 9 :$

pasberth

Syntax

Receiver message arg1 arg2 arg3 ==  self message receiver aeg1 arg2 arg3

self message returns a function whose type is receiver -> arg1 -> arg2 -> arg3 .

self message is undefined, but the message will be hooked by core function like AUTOLOAD,

pasberth

(ns macro-combinator
  (:refer-clojure :exclude [=]))
(defn prim [x] (fn [a] `(fn [~x] ~a)))
(defn in [v a] (v a))
(defn where [a v] (v a))
(defn = [v b] (fn [a] `(~(v a) ~b)))
(defn <- [v b] (fn [a] `(>>= ~b ~(v a))))

(println (in (= (prim 'x) 42) 'x))
; ((clojure.core/fn [x] x) 42)