kdxu

module A1 where


-- Bool 型
data Bool : Set where
  true : Bool
  false : Bool

-- パターンマッチや中値記法
_or_ : Bool -> Bool -> Bool 

kdxu

module A2 where

------------------------------------------------------
-- 述語論理
 
-- まずは命題論理から
 
-- 真(⊤)，偽(⊥)の定義が必要
-- ⊥ は証明がひとつもないような命題だから, 空集合によって表す
-- 帰納的定義によって次のように表現することができる

kdxu

package models

import dispatch._, Defaults._


object YoClient{

  val APIKey = "YOUR_YO_API_KEY"

  private def makeRequest(endpoint: String, args: Traversable[(String,String)]): Future[String] =

kdxu

module PolyP where
open import Function
open import Level

-----------------------------------------
----- polytypic programming in agda -----

data List {a} (A : Set a) : Set a where
  []  : List A
  Cons : (x : A) (xs : List A) → List A

kdxu

function poke(){
    var a = document.getElementsByTagName('a');
    for (var i=0;i<a.length;i++) { if (a[i].text == "Pokeを返す") a[i].click()}
}

setInterval(poke, 100);

kdxu

module PolyP where
open import Function
open import Level
open import Data.Nat 
-----------------------------------------
----- polytypic programming in agda -----

data List {a} (A : Set a) : Set a where
  []  : List A
  Cons : (x : A) (xs : List A) → List A

kdxu

module PolyP where
open import Function
open import Level
open import Data.Nat 
-----------------------------------------
----- polytypic programming in agda -----

data List {a} (A : Set a) : Set a where
  []  : List A
  Cons : (x : A) (xs : List A) → List A

kdxu

module mgu where

open import Data.Unit hiding (_≤_)
open import Data.Nat hiding (fold)
open import Data.Nat.Properties
open import Data.Fin hiding (_+_; _≤_; fold)
open import Data.Sum
open import Data.Product
open import Data.Maybe
open import Function using (_∘_)

kdxu

alias ls='ls -F'
alias ll='ls -la'
alias la='ls -a'
alias rails=''
alias emacs="/usr/local/Cellar/emacs/24.4/bin/emacs"
export EDITOR=/Applications/MacVim.app/Contents/MacOS/Vim
alias vim='env LANG=ja_JP.UTF-8 /Applications/MacVim.app/Contents/MacOS/Vim "$@"'
export PATH=$PATH:/usr/local/bin:~/Library/Haskell/bin
alias ochacaml='ledit ochacaml'
export SCALA_HOME=/Users/kyoko/scala-2.10.3

kdxu

alias ls='ls -F'
alias ll='ls -la'
alias la='ls -a'
alias rails=''
alias emacs="/usr/local/Cellar/emacs/24.4/bin/emacs"
alias ans='/Applications/Android\ Studio.app'
export EDITOR=/Applications/MacVim.app/Contents/MacOS/Vim
alias vim='env LANG=ja_JP.UTF-8 /Applications/MacVim.app/Contents/MacOS/Vim "$@"'
export PATH=$PATH:/usr/local/bin:~/Library/Haskell/bin
alias ochacaml='ledit ochacaml'