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 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_
View imgcat
#!/bin/bash
# tmux requires unrecognized OSC sequences to be wrapped with DCS tmux;
# <sequence> ST, and for all ESCs in <sequence> to be replaced with ESC ESC. It
# only accepts ESC backslash for ST.
function print_osc() {
if [[ -n $TERM ]] ; then
printf "\033Ptmux;\033\033]"
else
printf "\033]"
View EvalContML1.agda
module EvalContML1 where
open import Data.Nat as N using (ℕ)
open import Data.Bool as B using (Bool; false; true)
open import Relation.Binary.PropositionalEquality
data Value : Set where
int : Value
bool : Bool Value
You can’t perform that action at this time.