notogawa

{-# LANGUAGE GADTs #-}
{-# LANGUAGE FunctionalDependencies #-}

-- 0/1/二項演算op2 だけしか無い式の構文で，
-- 0が高々1回しか表れないようなものを表現し，
-- Eqのインスタンスにしたい．

class ContainsZeroAtMostOne a where

data WithZero

notogawa

#!/usr/bin/runhaskell
-- cabal install --with-ld=./gold.hs
import Data.List
import System.Environment
import System.Exit
import System.Process

ignores :: [String]
ignores = [ "--hash-size"
          , "--reduce-memory-overheads"

notogawa

// >=gcc-4.7
#include <iostream>
#include <type_traits>

// Universes
template < unsigned int Level >
struct Set {
    typedef Set< 1 + Level > type;
    typedef Set< Level > value;
    static const unsigned int level = Level;

notogawa

-- 饂飩はモノイドについて
-- https://twitter.com/tanakh/status/325586411191427073
--
module 饂飩 where

open import Data.List as List using (List; []; _∷_; _++_)
open import Algebra

data 基本味 : Set where
  たぬき : 基本味

notogawa

module CoqAgdaCorrespond where

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

-- Moduleはmodule
-- Definitionは非再帰関数
-- Fixpointは再帰関数

notogawa

------------------------------------------------------------------------
-- The Agda standard library
--
-- Rational numbers
------------------------------------------------------------------------

module Data.Rational where

import Algebra
import Data.Bool.Properties as Bool

notogawa

-- see. http://www.nicovideo.jp/watch/sm17339259
module RS3 where

open import Function
open import Function.Equivalence using (_⇔_; equivalence)
open import Data.Bool
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Product
import Relation.Binary.PropositionalEquality as PropEq

notogawa

module PFAD3 where

open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Function

infixr 2 _かつ_
_かつ_ = _×_

notogawa

module PFAD2 where

open import Function
open import Relation.Binary

module Ord {t₁ t₂ t₃} (T : DecTotalOrder t₁ t₂ t₃) where
  open import Data.List.NonEmpty
  open import Relation.Nullary

  open Relation.Binary.DecTotalOrder T

notogawa

module PFAD1 where

open import Function
open import Coinduction
open import Data.Bool
open import Data.List
open import Data.Colist
open import Data.Nat
open import Data.Product
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym)