ikedaisuke

module FooBarNat where

-- cheat on the exam; look the Standard library

Relation : Set -> Set -> Set1
Relation A B = A -> B -> Set

Reflexivity : (A : Set) -> Relation A A -> Set
Reflexivity A P = (i : A) -> P i i

ikedaisuke

module Agdacase where

data Nat : Set where
  zero : Nat
  succ : (n : Nat) -> Nat
-- an example : n += 2
succsucc : Nat -> Nat
succsucc n = {! !} -- try to type C-c C-c `in the goal'
-- then you should type the variable `n' in the minibuffer

ikedaisuke

{-# OPTIONS --universe-polymorphism #-}
module ReverseReverseId where

open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality 
  as P using (_≡_; refl; cong)

ReverseReverseId : ∀ {a} {A : Set a} (xs : List A) -> 
                   reverse (reverse xs) ≡ xs

ikedaisuke

Require Import Coq.Lists.List.

Lemma rev_Unfold : forall {A:Type} (l:list A) (a:A), rev (a::l) = rev l ++ (cons a nil).
Proof.
intros.
simpl.
reflexivity.
Qed.

Theorem rev_Involutive : forall {A:Type} (l:list A), rev (rev l) = l.

ikedaisuke

module EM where
{-
See also
http://www.cs.nott.ac.uk/~txa/g53cfr/l06.html/l06.html
-}

open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)

RAA : Set₁

ikedaisuke

-- An example of Gloss
-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_2

module Main where

import Graphics.Gloss

main :: IO ()
main
  = animateInWindow

ikedaisuke

module Main where

-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_0

import qualified Control.Monad.State as S
import Graphics.UI.GLUT

type AngleState a = S.StateT GLdouble IO a

timeOut :: Timeout

ikedaisuke

module Main where

-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_4

import Graphics.Gloss.Interface.Game

data State
  = State { angle :: Float
          , isPositive :: Bool
          , picture :: Picture }

ikedaisuke

module Main where

-- http://www.f13g.com/%A5%D7%A5%ED%A5%B0%A5%E9%A5%DF%A5%F3%A5%B0/Haskell/GLUT/#content_1_7

import System.Random
import Graphics.Gloss
import Graphics.Gloss.Interface.Simulate

data Particle
  = Particle { position :: Point

ikedaisuke

module Nat where

data Nat : Set where
  Z : Nat
  S : Nat -> Nat

data _plus_is_ : Nat -> Nat -> Nat -> Set where
  P-Zero : (m n : Nat) -> Z plus m is n
  P-Succ : (l m n : Nat) -> l plus m is n -> (S l) plus m is (S n)