▽低学歴無能俸給生活者の欧州移住計画
●02/02 02:45
FAQ / お問い合わせ窓口

▽mihoのお勉強ﾌﾞﾛｸﾞ（仮）
●02/01 20:52
FAQ / お問い合わせ窓口

▽F#雑記帳
●02/01 18:39
FAQ / お問い合わせ窓口

▽einblickerの日記
●02/01 13:39
FAQ / お問い合わせ窓口

▽So-net blog:Rainy Day Codings
●08/23 14:07
AgdaによるTaPL - Typed Arithmetic Expressions [Agda]
｢ﾌﾟﾛｸﾞﾗﾐﾝｸﾞ言語の基礎概念｣(五十嵐2011)をAgdaでやっていた途中だが､ ここで ”Types and Programming Language” (Pierce 2002) の第8章 ”Typed Arithmetic Expressions” をAgdaでやることにする｡
open import Relation.Binary.PropositionalEquality
using (_≡_; refl)
open import Data.Product
using (_×_; proj〓; proj〓; ∃; ∃-syntax) renaming (_,_ to 〓_,_〓)
open import Data.Sum using (_〓_; inj〓; inj〓)
Synta