maedaunderscore

(defun e2wm:dp-ensime ()
  (interactive)
  (e2wm:pst-change 'ensime))

(e2wm:pst-class-register
  (make-e2wm:$pst-class
   :name   'ensime
   :title  "Coding"
   :init   'e2wm:dp-ensime-init
   :main   'main

maedaunderscore

Definition reg := nat.
Definition label := nat.

Inductive instr : Set :=
| Imm :reg -> nat -> instr
| Copy : reg -> reg -> instr
| Jmp : label -> instr
| Jnz : reg -> label -> instr.

Definition regs := reg -> nat.

maedaunderscore

import sbt._
import Keys._
import Process._
import java.io.File
import java.awt.event._
import java.awt.TrayIcon._

object MyBuild extends Build {
  override lazy val projects = Seq(root)
  lazy val root = Project("root", file("."))  settings(

maedaunderscore

Option Explicit
Dim OBJ_FSO
Dim OBJ_Browser
Dim STR_ProgramName

Set OBJ_FSO = CreateObject("Scripting.FileSystemObject")

For Each OBJ_Browser In CreateObject("Shell.Application").Windows
  STR_ProgramName = OBJ_FSO.GetFileName(OBJ_Browser.FullName)
  If LCase(STR_ProgramName) = "iexplore.exe" Then

maedaunderscore

import scala.util.continuations._

object Main extends App{
  abstract sealed class Computation[+A]
  case class Yielded[A](k: Unit => Computation[A], v: A) extends Computation[A]
  case object Done extends Computation[Nothing]
  
  type yieldable[A] = cps[Computation[A]]

  def make[A] (body: (A => Unit @yieldable[A]) => Unit @yieldable[A]): Iterator[A] =

maedaunderscore

(* **** Exercise: 3 stars (optimize_0plus_b) *)
(** **** 練習問題: ★★★ (optimize_0plus_b) *)
Fixpoint optimize_bexp_0plus (e: bexp) : bexp :=
  match e with
  | BTrue => BTrue
  | BFalse => BFalse
  | BEq a1 a2 => BEq (optimize_0plus a1) (optimize_0plus a2)
  | BLe a1 a2 => BLe (optimize_0plus a1) (optimize_0plus a2)
  | BNot b => BNot (optimize_bexp_0plus b)
  | BAnd b1 b2 => BAnd (optimize_bexp_0plus b1) (optimize_bexp_0plus b2)

maedaunderscore

 Arith extends App {
  type Info = String

  sealed trait Term
  case class TmTrue(s: Info) extends Term
  case class TmFalse(s: Info) extends Term
  case class TmIf(s: Info, cond: Term, t: Term, f: Term) extends Term
  case class TmZero(s: Info) extends Term
  case class TmSucc(s: Info, t: Term) extends Term
  case class TmPred(s: Info, t: Term) extends Term

maedaunderscore

Theorem XtimesYinZ_spec : forall st a b st',
  st X = a ->
  st Y = b ->
  XtimesYinZ / st || st' ->
  st' Z = a * b.
Proof.

maedaunderscore

// https://gist.github.com/y-taka-23/8419128


mtype = { msg };

proctype Device(chan from_gcm){
  do
  :: from_gcm ? msg -> skip
  od
}

maedaunderscore

// ・Resonzのノイズは、各音の始まりだけに混じるようにする
// ・音が長いところは、後半にビブラートかける（音量に揺れができる）
// ・息継ぎがないので、どこかのタイミングで（１フレーズごと？）に音を切る
(
SynthDef(\main, { |out=0, note=81, next=81, dur=1, gate = 1, tempo=1, breath=0|
    var freq = [note, note+Rand(-0.02,0.02)!3, next].midicps;
    var d = dur / tempo;
    var t = d / 4.0;
    var freqEnv = EnvGen.ar(Env(freq, [t * 3, t], \exp));
    var cross = d / 32.0;