Skip to content

Instantly share code, notes, and snippets.

KINOSHITA Minoru krtx

Block or report user

Report or block krtx

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View unzip.dart
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);
}
View privacy policy
本アプリでは、個人情報は収集しません。
This app does not collect private information.
View hm.agda
module scratch where
open import Data.Nat
open import Data.Product
open import Relation.Nullary
postulate Dom : Set
Formula : Set₁
Formula zero = Set
View sk.ml
(* 演繹(論理式列)をツリーで表現する型 *)
type prop =
| Arg of int (* i番目の前提 *)
| App of prop * prop (* MP *)
| Axm of string (* 公理 *)
(* 演繹定理の(⇐)に相当する*)
let rec reduce_one = function
| Arg x ->
if x = 0
View tppmark2014.agda
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
View systemf.el
(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)))
View tapl24.f
/* --- --- --- --- --- --- --- --- --- --- --- --- --- --- */
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.
View open-record-agda.md

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

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

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

open import Data.Nat
View InfiniteChain.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
View tapl8.agda
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_
You can’t perform that action at this time.