This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
FROM debian | |
MAINTAINER Noriyuki OHKAWA <n.ohkawa@gmail.com> | |
RUN apt-get update | |
RUN apt-get install --no-install-recommends -y tomcat8 | |
ADD openam/OpenAM-12.0.0.war /var/lib/tomcat8/webapps/openam.war | |
EXPOSE 8080 | |
CMD /usr/lib/jvm/default-java/bin/java \ |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- uniqコマンド | |
-- | |
-- $ agda -c -i. -i/usr/share/agda-stdlib/ uniq.agda | |
-- $ ./uniq | |
-- | |
module uniq where | |
module PartialityStream where | |
open import IO using (IO; return; _>>=_) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} | |
module Flatten (flatten) where | |
import Control.Monad | |
class Flatten m x a where | |
flatten :: x -> m a | |
instance Monad m => Flatten m (m a) a where | |
flatten = id |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE QuasiQuotes #-} | |
{-# LANGUAGE TemplateHaskell #-} | |
{-# LANGUAGE OverloadedStrings #-} | |
module Main where | |
import qualified Language.C.Inline as C | |
import Foreign.C.Types | |
import Foreign.C.String | |
C.include "python2.7/Python.h" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE FlexibleContexts #-} | |
module Data.JQ where | |
import Control.Applicative ( Applicative, (<$>), (<*>) ) | |
import Control.Monad ( (>=>) ) | |
import Control.Monad.Reader.Class | |
import qualified Data.Aeson as JSON | |
import qualified Data.Aeson.Types as JSON | |
import qualified Data.HashMap.Strict as HM | |
import Data.List ( foldl1' ) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE MultiParamTypeClasses #-} | |
{-# LANGUAGE FlexibleInstances #-} | |
import Prelude hiding ( (+) ) | |
import qualified Prelude as P | |
class FuzzyAddable a b c where | |
(+) :: a -> b -> c | |
instance FuzzyAddable String Int String where | |
a + b = a ++ show b | |
instance Num a => FuzzyAddable a a a where |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- 各データ型に対する帰納法の定義を考えると, | |
-- ≡の定義の仕方(parameter1つとindex1つ/index2つ)による差がわかる | |
module Ind where | |
-- ℕ | |
data ℕ : Set where | |
zero : ℕ | |
suc : ℕ → ℕ | |
-- ℕに関する帰納法 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Test where | |
open import Relation.Binary.PropositionalEquality | |
postulate | |
extensionality : ∀ {a} {b} {A : Set a} {B : A → Set b} {f g : (x : A) → B x} → (∀ x → f x ≡ g x) → f ≡ g | |
covariant : {B : Set} → (B → B → B) → {A : Set} → (A → B) → (A → B) → (A → B) | |
covariant _⊕_ f g = λ x → f x ⊕ g x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
open import Category.Monad | |
module DoLikeNotation {l M} (monad : RawMonad {l} M) where | |
open RawMonad monad | |
bind-syntax = _>>=_ | |
syntax bind-syntax F (λ x → G) = ∣ x ← F ∣ G |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Test where | |
open import Function | |
open import Data.Empty | |
open import Data.Nat | |
open import Data.Nat.Properties | |
open import Data.Nat.DivMod using (_divMod_; _mod_; result) | |
open import Data.Fin using (zero; suc; toℕ) | |
open import Data.Sum | |
open import Data.Product |