notogawa

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

module Data.Rational where

import Algebra
import Data.Bool.Properties as Bool

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

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

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

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

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

#!/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

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

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

class ContainsZeroAtMostOne a where

data WithZero

notogawa

-- AをaにBをbにeps近似で，めんどうなので 0 < a, 0 < b に限定するけど
innerQ :: Rational -> Rational -> Rational
innerQ a b | a > b = innerQ b a
innerQ a b = head $ [1 .. d 1] >>= f 1 where
    -- マジメにやるなら2分探索とか
    d n | 1 / n < b - a = n | otherwise = d (n+1)
    f n x | b < n / x = []
          | a < n / x && n / x < b = [n / x] -- 近似時のeps分も入れれば確実にAとBの間に入る
          | n / x < a = f (n+1) x

notogawa

-- http://people.inf.elte.hu/divip/AgdaTutorial/Functions.Equality_Proofs.html
module Theorem where

import Level

data ℕ : Set where
  zero : ℕ
  suc  : (n : ℕ) → ℕ

{-# BUILTIN NATURAL ℕ    #-}

notogawa

#define Q(c)*q=#c;c
Q(main(n){for(scanf("%d",&n);n--;)printf("#define Q(c)*q=#c;c\nQ(%s)",q);})

notogawa

;;; -*- mode: emacs-lisp; coding: utf-8-unix; indent-tabs-mode: nil -*-

(when (require 'haskell-mode nil t)
  (when (require 'haskell-cabal nil t)
    (autoload 'offside-trap-mode "mode/haskell/offside-trap/offside-trap.el")

    (add-to-list 'auto-mode-alist '("\\.[hg]s$" . haskell-mode))
    (add-to-list 'auto-mode-alist '("\\.hi$" . haskell-mode))
    (add-to-list 'auto-mode-alist '("\\.l[hg]s$" . literate-haskell-mode))
    (add-to-list 'auto-mode-alist '("\\.cabal\\'" . haskell-cabal-mode))