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

qnighy

はじめに

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

HoTTの参考資料

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

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

kdxu

module A2 where

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

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

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

ashiato45

sig Element{}

one sig Group{
	elements: set Element,
	unit: one elements,
	mult: elements -> elements -> one elements,
	inv: elements -> one elements
}

fact NoRedundantElements{

cutsea110

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures,
             TypeSynonymInstances,
             FlexibleInstances
#-}
module FixPrime where

import Prelude hiding (Functor(..), map, succ, either)

pair (f, g) x = (f x, g x)

ekmett

-- http://comonad.com/reader/2018/the-state-comonad/
-- https://www.reddit.com/r/haskell/comments/7oav51/i_made_a_monad_that_i_havent_seen_before_and_i/

{-# language DeriveFunctor #-}

import Control.Comonad
import Data.Semigroup

data Store s a = Store { peek :: s -> a, pos :: s } deriving Functor

WhiteCat6142

bsort=foldr bs []
 where bs x []=[x]
       bs x (y:ys)|x<=y =(x:y:ys)
                  |otherwise =(y:bs x ys)

nyuichi

; -*- mode: scheme;-*-
; Implementation of resolution principle for first-order logic in Egison

(define $unordered-pair
 (lambda [$m]
  (matcher
    {[<pair $ $> [m m] {[[$x $y] {[x y] [y x]}]}]
     [$ [something] {[$tgt {tgt}]}]})))

(define $positive?