Skip to content

Instantly share code, notes, and snippets.

View krtx's full-sized avatar

KINOSHITA Minoru krtx

19 followers · 20 following
View GitHub Profile
@krtx
krtx / unzip.dart
Created July 29, 2019 13:16
import 'dart:io';
import 'dart:convert';
import 'package:args/args.dart';
// read bytes into integer in little endian
getBytes(List<int> bytes, int offset, int length) {
int res = 0;
for (var i = 0; i < length; i++) {
res += bytes[i + offset] << (i * 8);
}
@krtx
krtx / privacy policy
Created July 2, 2019 05:09
本アプリでは、個人情報は収集しません。
This app does not collect private information.
@krtx
krtx / hm.agda
Last active May 30, 2018 18:10
module scratch where
open import Data.Nat
open import Data.Product
open import Relation.Nullary
postulate Dom : Set
Formula : ℕ → Set₁
Formula zero = Set
@krtx
krtx / sk.ml
Last active May 24, 2018 02:10
(* 演繹(論理式列)をツリーで表現する型 *)
type prop =
| Arg of int (* i番目の前提 *)
| App of prop * prop (* MP *)
| Axm of string (* 公理 *)
(* 演繹定理の(⇐)に相当する*)
let rec reduce_one = function
| Arg x ->
if x = 0
@krtx
krtx / tppmark2014.agda
Created July 5, 2017 10:52
open import Function
open import Data.Empty
open import Data.Nat
open import Data.Nat.Properties.Simple
open import Data.Nat.Divisibility
open import Data.Sum
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Induction.Nat
open import Induction.WellFounded
@krtx
krtx / systemf.el
Created June 8, 2017 03:28
(defvar systemf-mode-syntax-table nil "Syntax table for systemf mode.")
(setq systemf-mode-syntax-table
(let ((syn-table (make-syntax-table)))
(modify-syntax-entry ?\/ ". 14" syn-table)
(modify-syntax-entry ?* ". 23" syn-table)
syn-table))
(defface systemf-lock-governing-face
'((t (:foreground "black" :weight bold)))
@krtx
krtx / tapl24.f
Created June 8, 2017 03:27
/* --- --- --- --- --- --- --- --- --- --- --- --- --- --- */
Pair = lambda X. lambda Y. All R. (X -> Y -> R) -> R;
pair = lambda X.
lambda Y.
lambda x: X.
lambda y: Y.
lambda R.
lambda p: X -> Y -> R.
@krtx
krtx / open-record-agda.md
Created May 31, 2017 10:26

下の１文で ≤-trans が使える理由

open DecTotalOrder decTotalOrder using () renaming (trans to ≤-trans)

レコード型のあるフィールドにアクセスするためには 型名.射影関数 そのレコード型の値 と書く必要があります。

open import Data.Nat
@krtx
krtx / InfiniteChain.agda
Created February 5, 2017 16:43
http://adam.chlipala.net/cpdt/html/GeneralRec.html#noBadChains in Agda
module InfiniteChain where
-- http://adam.chlipala.net/cpdt/html/GeneralRec.html#noBadChains in Agda
open import Induction.WellFounded
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
record Stream (A : Set) : Set where
coinductive
@krtx
krtx / tapl8.agda
Last active January 22, 2017 17:33
module tapl8 where
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Data.Star
open import Data.Empty
infix 5 if_then_else_