greymd

; ひねくれた方法な気がする。

(map
    3#(match [%1 %2 %3] something {
      [[_ ,0 ,0] FizzBuzz]
      [[_ ,0 _] Fizz]
      [[_ _ ,0] Buzz]
      [[$i _ _] i]})
        (map 1#[%1 (modulo %1 3) (modulo %1 5)] (take 100 nats)))

PhilOwen

import Control.Concurrent
import Control.Monad
import System.RaspberryPi.GPIO

main :: IO ()
main = withGPIO $ do
  let p = PinV1_13
  setPinFunction p Output
  forever $ do  
    writePin p True

kdxu

module A2 where

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

qnighy

はじめに

HoTT(ホモトピー型理論) はホモトピー論や∞圏論を型システムの上で展開しようという考え方である。この体系は既にCoqで形式化が進んでいる。これはその使い方の覚書である。

HoTTの参考資料

まず、HoTT/Coqではなく、HoTT全般に関係する資料について述べる。

• HoTTの本家サイト http://homotopytypetheory.org/ に情報がたくさんある。この分野は数学の他分野に比べて、インターネット上に情報がより集約されているという特徴がある。
• HoTTについて紙面で勉強するならば、上のサイトにあるHoTT Bookを読むのが最も適切である。

msakai

// うみねこのなく頃に8 のベルンの挑戦のAlloyモデル
abstract sig Person { kill : set Person }
one sig
  Krauss, Natsuhi, Jessica,
  Eva, Hideyoshi, George, 
  Rudolf, Kyrie, Battler,
  Rosa, Maria,
  Nanjo,
  Genji, Shannon, Kanon, Gouda, Kumasawa
  extends Person {}