Skip to content

Instantly share code, notes, and snippets.

View ikedaisuke's full-sized avatar

Ikegami Daisuke ikedaisuke

27 followers · 2 following
  • Japan
View GitHub Profile
@ikedaisuke
ikedaisuke / gist:1211203
Created September 12, 2011 13:03
Peano axioms of natural numbers in Agda
module Peano where
open import Data.Nat using (ℕ; zero; suc)
open import Relation.Binary.Core using (_≢_; refl)
{-
already defined:
data ℕ : Set where
zero : ℕ -- axiom 1
suc : (n : ℕ) -> ℕ -- axiom 2
@ikedaisuke
ikedaisuke / gist:1305738
Created October 22, 2011 07:20
dart (bleeding_edge rev. 623) の型検査バグ? ではなく、型検査オプションが必要だという話でした
foo() {
List<List<int>> arr;
arr[0] = 0; // no error nor warning
arr = 0; // ditto
}
main() {}
// % dart foo.dart
// %
// % dart --enable_type_chekcs foo.dart
@ikedaisuke
ikedaisuke / gist:1344224
Created November 7, 2011 05:10
Thierry's proof of the principle of infinite descent (a part) in Agda1/Alfa
noether (A::Set)(R::rel A) :: Type
= (P::pred A) -> ((x::A) -> ((y::A) -> R y x -> P y) -> P x) -> (x::A) -> P x
infiniteDescent (A::Set)
(R::rel A)
(P::pred A)
:: noether A R ->
((x::A) -> P x -> exists A (\(x1::A) -> and (R x1 x) (P x1))) ->
(x::A) -> not (P x)
= \ (h1::noether A R) ->
\ (h2::(x::A) -> P x -> exists A (\(x1::A) -> and (R x1 x) (P x1))) ->
@ikedaisuke
ikedaisuke / gist:1344227
Created November 7, 2011 05:12
Thierry's proof of the principle of infinite descent (a part) in Agda2
infiniteDescent : ∀ {a l} -> (A : Set a) -> (R : Rel A l) ->
(P : Pred A l) -> Noether A R ->
((x : A) -> P x -> ∃ (λ y -> R y x × P y)) ->
(z : A) -> ¬ (P z)
infiniteDescent A R P noe f
= noe (λ w → ¬ P w) g
where g : (x : A) → ((y : A) → R y x → ¬ P y) → ¬ P x
g x h px with f x px
... | (v , k) = h v (proj₁ k) (proj₂ k)
@ikedaisuke
ikedaisuke / gist:1376024
Created November 18, 2011 09:47
TPPmark 写経途中
module Half where
-- http://staff.aist.go.jp/reynald.affeldt/tpp2011/garrigue_candy.v
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.Core
open import Relation.Binary.PropositionalEquality
half : ℕ -> ℕ
@ikedaisuke
ikedaisuke / gist:1408300
Created November 30, 2011 07:05
Yet another program in Haskell to pretty-print and parse files
module Main where
-- see also Shugo's blog
-- http://shugo.net/jit/20111129.html#p01
import Control.Applicative
import Data.List
import System.Environment
import System.IO
import qualified Text.ParserCombinators.Parsec as PC
@ikedaisuke
ikedaisuke / Noricoco.agda
Created May 30, 2012 10:34
@noricoco gives an exercise.
module Noricoco where
-- Hello! See also
-- http://togetter.com/li/312309
open import Data.Empty using (⊥-elim)
open import Data.Nat using (_≟_; ℕ)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Binary.PropositionalEquality using (_≡_)
open import Relation.Nullary using (yes; no)
@ikedaisuke
ikedaisuke / Homework.hs
Created November 30, 2012 10:58
Answers of the homework in the slides
-- http://www.slideshare.net/yashigani/haskell-in/19
module Homework where
import Data.List(foldl')
myNull :: [a] -> Bool
myNull [] = True
myNull _ = False
@ikedaisuke
ikedaisuke / gist:4175351
Created November 30, 2012 11:54
Some answers of the homework in the slides
-- http://koko-u.github.com/haskell_book_reading/#25
import Data.Char (toUpper, intToDigit, isSpace)
import Data.List (isInfixOf, nub)
import Numeric (showIntAtBase)
upperCase :: String -> String
upperCase = map toUpper
removeSpaces :: String -> String
@ikedaisuke
ikedaisuke / gist:5253746
Created March 27, 2013 12:14
2013-03-27 すごいHaskell読書会 in 大阪 #7 の課題について
@yashigani さんの出題した課題の設計方針を書きます
問題はこちら：
https://gist.github.com/yashigani/5231928
上記資料の一番下に課題があります。
転載：
-----