mizunashi-mana

{-# LANGUAGE RankNTypes    #-}
{-# LANGUAGE TypeOperators #-}

module NatTrans where

import Data.Foldable
import Data.Functor.Identity


newtype f :~> g = NT

mizunashi-mana

APIが壊れないプログラミング言語

目的

以下を満たすプログラミング言語を目指す．

• APIのバージョンをコントロールできる．
• APIの変更を検査し，変更が破壊的であるかを保証できる．

mizunashi-mana

Require Import Arith.

Fixpoint sum (n: nat) {struct n}: nat :=
  match n with
  | O   => O
  | S p => S p + sum p
  end.

Lemma sum_Sn: forall n, sum (S n) = S n + sum n.
Proof.

mizunashi-mana

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE UndecidableInstances #-}

module Data.DeferIsPrime where

mizunashi-mana

{-# LANGUAGE ImplicitPrelude #-}

module Control.Concurrent.Async.Extra where

import           Control.Concurrent.Async
import           Control.Monad.Trans.Except
import           Data.Foldable

concurrentlyExcept :: IO (Except e a) -> IO (Except e b) -> IO (Except e (a, b))
concurrentlyExcept actA actB = do

mizunashi-mana

import           Control.Applicative
import qualified Text.Parsec         as P
import           Text.Parsec.String

data Command = Command
        { addr    :: Maybe Addr
        , cmdName :: Char
        , param   :: Maybe String
        } deriving (Show, Eq)

mizunashi-mana

ed :: [String] -> IO ()
ed args = if null args
  then do
    x <- fromMaybe "" <$> runInputT defaultSettings (getInputLine "")
    ed' (setCmd x) [] [] 1 True
  
  else do
    x <- createBuffer (head args)
    y <- fromMaybe "" <$> runInputT defaultSettings (getInputLine "")
    ed' (setCmd y) (head args) x 1 True

mizunashi-mana

module Works.TestParsec where

import Text.Parsec hiding (optional)
import Text.Parsec.String

import Control.Applicative (optional)

data Command = Command
  { address :: Maybe Address
  , cmdName :: Char

mizunashi-mana

Pillow==3.3.1

mizunashi-mana

Nested Unordered List Example

For gitbook bug report:

• Item 1

  Item 1 text