krtx

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

本アプリでは、個人情報は収集しません。

This app does not collect private information.

krtx

module scratch where

open import Data.Nat
open import Data.Product
open import Relation.Nullary

postulate Dom : Set

Formula : ℕ → Set₁
Formula zero    = Set

krtx

(* 演繹(論理式列)をツリーで表現する型 *)
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

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

(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

/* --- --- --- --- --- --- --- --- --- --- --- --- --- --- */

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

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

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

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

open import Data.Nat

krtx

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

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_