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

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 A2 where

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

kdxu

module A1 where


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

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

kdxu

module A2 where

------------------------------------------------------
-- 一階命題論理

-- まずは，ふつうの命題論理から


-- 真(⊤)，偽(⊥)の定義が必要
-- ⊥ は証明がひとつもないような命題だから, 空集合によって表す

kdxu

module A2 where

open import Data.Nat
open import Data.Bool hiding(_∧_;_∨_)

------------------------------------------------------

-- ⊥ は証明がひとつもないような命題だから, 空集合によって表す
-- 帰納的定義によって次のように表現することができる
data ⊥ : Set where

kdxu

 private module H = ≅-Reasoning
 
 Γ5 : Cxt {1 + m2} n
 Γ5 = substCxt (σ2' ⊹⊹ σ1') (liftCxt (count (App s1 s2)) Γ)
 
 -- として，
 
 eq : Γ3 ≅ Γ4
                        eq =
                          H.begin

kdxu

- (void)imagePickerController:(UIImagePickerController *)picker didFinishPickingMediaWithInfo:(NSDictionary *)info{
    // Pathを取得
    UIImage *pickedImage = (UIImage *)[info objectForKey:UIImagePickerControllerOriginalImage];
    if (pickedImage) {
        NSData *data = [[NSData alloc] initWithData:UIImagePNGRepresentation(pickedImage)];
        [DBAccess updatePic:@{@"cl_id":[NSString stringWithFormat:@"%d",cl_id], @"pic":data}];
    }

    // モーダルビューを閉じる
    if (![_cameraviewcontroller.presentedViewController isBeingDismissed]) {

kdxu

//
//  DBAccess.m
//  enpittest
//
//  Created by SayuriAnbe on 2014/08/27.
//  Copyright (c) 2014年 SayuriAnbe. All rights reserved.
//

#import "DBAccess.h"

kdxu

#pragma strict
private var startTime:float;
private var lapTime:float;
var score : int = 0;
private var max : int;
private var maxs : int = 60;
private var stop : boolean = false;
private var style : GUIStyle; 
function Update () {
    if (score >= max || lapTime >= maxs) {