Skip to content

Instantly share code, notes, and snippets.

View simplex_category.v
Require Import Relation_Definitions.
Require Import SetoidClass.
Require Import VectorDef.
Require Import Morphisms.
Require Import COC.Base.Main.
Set Implicit Arguments.
@as-capabl
as-capabl / ReaderTImpl.v
Created Jun 27, 2016
やりたいこと:Coq上でReaderTを実装し、Haskellコードに変換してHaskell側から使う
View ReaderTImpl.v
(* やりたいこと:Coq上でReaderTを実装し、
Haskellコードに変換してHaskell側から使う *)
Require Import Coq.Logic.FunctionalExtensionality.
Section Monad_Definition.
(* Reserved Notation "c >>= f"
(at level 42, left associativity). *)
(* Monadの宣言 *)
Class Monad {T : Type -> Type} (returns : forall {A : Type}, A -> T A)
View benchmark.hs
{-# LANGUAGE Arrows #-}
module Main where
import Prelude hiding (filter, id, (.), unzip, mapM_)
import Control.Category
import Control.Arrow
import Criterion
import Criterion.Main (defaultMain)
import Data.Time
@as-capabl
as-capabl / filter.hs
Last active Aug 29, 2015
A filter implementation on objective
View filter.hs
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RankNTypes #-}
module
Main
where
@as-capabl
as-capabl / freemonoid.v
Created Mar 1, 2015
List as free monoid.
View freemonoid.v
Require Import List.
Section Monoid.
Class Monoid {A:Type} (dot : A -> A -> A) (unit : A) : Prop :=
{
dot_assoc :
forall x y z:A,
dot x (dot y z) = dot (dot x y) z;
unit_left :
forall x, dot unit x = x;
View objpipe.hs
{-# Language GADTs #-}
{-# Language RankNTypes #-}
{-# Language TypeOperators #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language MultiParamTypeClasses #-}
{-# Language FlexibleInstances #-}
{-# Language LambdaCase #-}
module
Main
View 1-intro.hs
{-# Language Arrows #-}
import Control.Arrow
import Control.Monad (forever)
import Control.Monad.Trans (lift)
import qualified Control.Arrow.Machine as P
import qualified Data.Machine as Mc
import Data.Machine ((<~))
You can’t perform that action at this time.