notogawa

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds #-}
module Main where

import Prelude hiding ((.), Word)
import qualified Prelude
import Data.Singletons

notogawa

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Siri where

import GHC.TypeLits (Nat)

notogawa

ghc-8.2.1-rc1でcabal-installを試すにはcabalのリポジトリe4c36b9dd時点に， このパッチ当てて

EXTRA_CONFIGURE_OPTS="--allow-newer=base,time" ./bootstrap.sh

あと，配布されてる ghc-8.2.0.20170404-x86_64-deb8-linux.tar.xz はjesssieだとリンクに失敗するのでsidにしとくといい

notogawa

function init-prompt-git-branch()
{
  git symbolic-ref HEAD 2>/dev/null >/dev/null &&
  echo "($(git symbolic-ref HEAD 2>/dev/null | sed 's/^refs\/heads\///'))"
}

if which git 2>/dev/null >/dev/null
then
  export PS1_GIT_BRANCH='\[\e[$[COLUMNS]D\]\[\e[1;31m\]\[\e[$[COLUMNS-$(length $(init-prompt-git-branch))]C\]$(init-prompt-git-branch)\[\e[$[COLUMNS]D\]\[\e[0m\]'
else

notogawa

module C where

import Relation.Binary.PropositionalEquality as PropEq
open PropEq using (_≡_; refl)

data C {A : Set} : Set where
  c : (a : A) → C

------ ケース1
-- OK

notogawa

{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}

import Data.Singletons
import Data.Singletons.Prelude.Enum
import Data.Singletons.Prelude.List
import Data.Singletons.Prelude.Num
import GHC.TypeLits

notogawa

module ET where

open import Data.Maybe                                                                                                     
open import Data.Nat
open import Data.Bool using (Bool; true)
open import Data.Product using (∃; _,_; _×_)
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary using (Dec; yes; no)

data TypeRep : Set where

notogawa

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
import Data.Proxy
import Data.Singletons
import Data.Singletons.TypeLits
import Data.Type.Equality
import GHC.TypeLits

notogawa

module Main where

import Network ( withSocketsDo, listenOn, PortID(PortNumber), connectTo )
import Network.Socket ( accept, send, close, recvLen )
import Control.Concurrent ( forkIO, threadDelay )
import System.IO ( hClose )
import Control.Monad ( void )
import Control.Exception ( bracket )

main :: IO ()

notogawa

-- FLOPS 2016 Agda Tutorial
module FLOPS2016 where

-- 歴史の話
-- ALF Half Agda1 ALFA AgdaLight Agda2

-- Simply Typed Lambda Calculus
--   Checking Inference Lookup Rules

data ℕ : Set where