myuon

(when load-file-name
  (setq user-emacs-directory (file-name-directory load-file-name)))

(add-to-list 'load-path (locate-user-emacs-file "el-get/el-get"))
(unless (require 'el-get nil 'noerror)
  (with-current-buffer
      (url-retrieve-synchronously
       "https://raw.githubusercontent.com/dimitri/el-get/master/el-get-install.el")
    (goto-char (point-max))
    (eval-print-last-sexp)))

myuon

import Function
open import Data.Unit.Base hiding (_≤_)
open import Data.Empty
open import Data.Product
open import Data.Sum
open import Data.List as L
open import Data.List.Any
open import Data.Fin hiding (_≤_; _<_; _+_)
open import Data.Nat
open import Data.Nat.Properties

myuon

open import Data.List

mutual
  data Typ : Set₁ where
    ground : Set → Typ
    tyw : Typ → Subst → Typ

  data Subst : Set where
    id : Subst
    ↑ : Subst

myuon

--track0:加速度,0,500,50
--track1:Y移動量,-1000,1000,500
--track2:弾性係数,0,10.00,0.80
--track3:閾値,0.1,100,0.1
--check0:高さ0地点からスタート,0;
--dialog:バウンド回数,bmax=-1;

g = obj.track0
H = obj.track1
e = obj.track2

myuon

import init data.list data.nat
open nat list eq.ops

lemma filter_length_bound {p : nat → Prop} [h : decidable_pred p] : ∀ {xs : list nat}, length (filter p xs) ≤ length xs
| [] := by simp
| (x::xs) := match decidable.em (p x) with
  | (or.inl px) := calc
    length (filter p (x::xs)) = length (x :: filter p xs) : !filter_cons_of_pos px ▸ rfl
    ... = length (filter p xs) + 1 : by simp
    ... ≤ length xs + 1 : add_le_add_right !filter_length_bound 1

myuon

> f(x,T) = x < (T/4.0) ? 0 : (T/4.0 <= x && x < T) ? (4.0/9.0)*(1.0/(T**2))*(x-T/4.0)**2 : (T <= x && x < 2 * T) ? (0.6/(T**2))*(x-T)**2 + 0.25 : 0.25*log10(x / (2.0*T)) + 0.85
> plot [0:100] f(x,20)

myuon

実際にオフラインでやったときのレポート：
・PL4人で実質4〜5時間くらいかかった？
・PLは早苗の先輩Sさん、知り合いの考古学者Kさん、雄太の同級生Iくん、IとKの知り合いの医師Kさんの4人
・3人がD大学関係者だったせいでD大学付近ばかりの探索になってしまい、意外と難航した
・なぜか東山家へピザを持って押し入るという展開に
・最後は山間の湖でアンデッド譲司と殴り合い(グラーキはこの際出さなかったが、召喚の途中だったのでターン経過で召喚するなどしてもよかった)
・脳筋Iくんの組みつきとマーシャルアーツが強すぎ/戦闘のルールは事前に全員で確認しよう
・2/4人が不定の狂気 2人は正常のまま譲司のみを倒した。緑の崩壊を使ったので死体は残らず、殺人容疑がかけられることもなく終了。

myuon

つり目 http://melpon.org/wandbox/permlink/A2Or72SjdTcSYF18
縞ニーソ http://melpon.org/wandbox/permlink/GZNJFElV3dQGUQ6p
カーディガン http://melpon.org/wandbox/permlink/YgK1sGzMjLRBSxdn
ツインテール http://melpon.org/wandbox/permlink/JutUOzLsJiP2uS1I
めがね http://melpon.org/wandbox/permlink/XG39WvBjayBqxh8k

myuon

import Control.Monad.Cont

runC :: Cont w w -> w
runC m = runCont m id

reset :: Cont a a -> Cont w a
reset = return . runC

shift :: ((a -> w) -> Cont w w) -> Cont w a
shift f = cont (runC . f)

myuon

import init.setoid
import data.set
open set

structure category [class] :=
  (obj : Type)
  (hom : obj → obj → Type)
  (id : ∀ (x : obj), hom x x)
  (comp : ∀ {a b c : obj}, hom b c → hom a b → hom a c)
  (assoc : ∀ {a b c d} {f : hom a b} {g : hom b c} {h : hom c d},