Skip to content

Instantly share code, notes, and snippets.

This file has been truncated, but you can view the full file.
1 1 1
A0 0 0
F_SHIFT_PUTC
o0 1 1
o1 1 1
o2 1 1
o3 1 1
o4 0 0
o5 0 0
o6 1 1
5ページ 2行目、M^abc(l, h) は M^abc(l, g)
16ページ 最後の図式の一番右の id_c・λ_(g・f) は λ_{id_c・(g・f)} (消すid_cがずれてる)
17ページ 最初の図式、ところどころ id_c が id になってる
30ページ 最初の図の一番下のαはα^-1
33ページ 一番下の式の3行目()が一個よけい
43ページ 証明の真ん中あたり、φ_gpはφ_qp
52ページ ∵の最初の赤い丸のあたり、βとγが一か所typo
52ページ ω_a(u)_sが関手であることを示した後に、ω_aが関手であることも示さないといけなくない?
ω_aの射の行先ω_a(f)を決めた後に、Δの確認のところで、θ_a(ω_a(f))=P(id_a)(f)も確かめないといけなさそう。
(ω_a(u)_p)_g := φ_pg で定義することも書かないと54ページの定義より~がおかしくなりそう。
@kik
kik / LucasLehmer.v
Created July 31, 2016 06:39
Lucas–Lehmer primality test by Coq
From mathcomp
Require Import all_ssreflect.
From mathcomp
Require Import ssralg ring_quotient finalg poly polydiv zmodp.
From mathcomp
Require Import all_fingroup cyclic.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
@kik
kik / B.v
Last active April 16, 2016 14:29
GCJ 2016 予選B問題
Require Import Arith Even Bool List Omega.
Local Coercion is_true : bool >-> Sortclass.
Set Implicit Arguments.
(*
* 問題の定義
*)
Definition happiest (ps : list bool) : bool :=
@kik
kik / d.rb
Created April 12, 2015 10:26
GCJ2015 Q D
G = 'GABRIEL'
R = 'RICHARD'
def solve(x, r, c)
#p [x, r, c]
if r > c
r, c = c, r
end
# r <= c
@kik
kik / 1p.cc
Created March 1, 2015 18:55
TLE 2015
#include <set>
#include <string>
#include <iostream>
using namespace std;
int main()
{
int T;
cin >> T;
char buf[2048];
cin.getline(buf, 2048);
@kik
kik / socket.dats
Created January 12, 2015 16:16
ATS2でリソース管理。ソケット開いて閉じるだけ。普通のcloseでは失敗する場合のある闇
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
staload S = "libc/sys/SATS/socket.sats"
extern
fun socket(af: $S.sa_family_t, st: $S.socktype_t, proto: int) : [fd:int]
(
option_v ($S.socket_v (fd, $S.init), fd >= 0) | int(fd)
) = "mac#socket"
@kik
kik / t.dats
Created January 11, 2015 17:28
初めてのATS2。見たとおりのCのコードにコンパイルされた
#include "share/atspre_define.hats"
#include "share/atspre_staload.hats"
fn foo1(n : bool, dst : &int) : bool =
if n then (
dst := 42;
true
) else (
dst := 0;
false
@kik
kik / README.txt
Created October 11, 2014 16:48
ArduinoによるAMラジオテスト用の信号発生器
ブレッドボードで作ったAMラジオが全然動かないので、Arduino Leonardでお手軽に作ったAMラジオの信号発生器
搬送波は1MHzで矩形波なので高調波が乗りまくってると思われる。
音声信号は500-1000Hzぐらいの音階で矩形波。
AM変調は搬送波をon/offするだけ。
5番ピンに適当な長さの電線を繋いでバーアンテナに近づけると動く。
(defun show-current-char ()
(let ((ch (following-char)))
(format " [U+%04X %s] " ch (get-char-code-property ch 'name))))
(easy-mmode-define-minor-mode show-char-mode
"Toggle Show char mode."
t
(:eval (show-current-char)))