myuon

Require Import Morphisms Setoid.
Require Import Utf8.

Require Program.Basics.
Module Func := Basics.

Require SetoidClass.
Module SC := SetoidClass.

Set Implicit Arguments.

myuon

Notation "`Begin p" := p (at level 20, right associativity).
Notation "a =] p ] pr" := (@eq_trans _ a _ _ p pr) (at level 30, right associativity).
Notation "a =[ p [ pr" := (@eq_trans _ a _ _ (eq_sym p) pr) (at level 30, right associativity).
Notation "a `End" := (@eq_refl _ a) (at level 10).

Proposition congr {A B : Type} {a b : A} (P : A -> B) (p : a = b) : P a = P b.
  rewrite p. reflexivity.
Qed.

Inductive list (T: Type) : Type :=

myuon

#! /usr/bin/env python
#-*- coding:utf-8 -*-
import io
import sys

def transpose(xs):
    return list(map(list, zip(*xs)))

def deascii(d):
    if d == '-': return 0

myuon

{-# OPTIONS --no-positivity-check #-}
open import Data.Nat
open import Data.Vec as Vec
open import Data.Star
open import Data.Empty
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module SN {ConTm ConTy : Set} {B-length} (Base : Vec (ConTm × ConTy) B-length) where

myuon

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
module Mu where

import Data.Maybe (fromJust)
import qualified Data.Map as M
import qualified Data.Set as S
import Data.List
import Control.Monad.State

myuon

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE DataKinds, GADTs, TypeFamilies, PolyKinds, TypeOperators #-}
{-# LANGUAGE RankNTypes, TypeApplications #-}
import Prelude(($), putStrLn)

-- equality

infix 2 ==
data (==) :: k -> k -> * where
  Refl :: a == a

myuon

type expr =
  | MLplus | MLequal | MLfst | MLsnd
  | MLint of int
  | MLbool of bool
  | MLvar of string
  | MLcond of expr * expr * expr
  | MLpair of expr * expr
  | MLin of dec * expr
  | MLabstr of pat * expr
  | MLapp of expr * expr

myuon

#
# Executes commands at the start of an interactive session.
#
# Authors:
#   Sorin Ionescu <[email protected]>
#

# Source Prezto.
if [[ -s "${ZDOTDIR:-$HOME}/.zprezto/init.zsh" ]]; then
  source "${ZDOTDIR:-$HOME}/.zprezto/init.zsh"

myuon

# prefixキーをC-aに変更する
set -g prefix C-z

# C-bのキーバインドを解除する
unbind C-b

# キーストロークのディレイを減らす
set -sg escape-time 1

# ウィンドウのインデックスを1から始める

myuon

import * as $ from "jquery";

function extend<T extends U, U>(itrf: T, part: U): T {
  return $.extend(itrf, part);
}

// --------

interface Test {
  poyo: string,