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

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

{-# 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

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

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