takeouchida

import matplotlib.pyplot as plt
from matplotlib import cm
from matplotlib.ticker import LinearLocator
import numpy as np

fig, ax = plt.subplots(subplot_kw={"projection": "3d"})
x = np.arange(-5, 5, 0.25)
y = np.arange(-5, 5, 0.25)
x, y = np.meshgrid(x, y)
z = x * x + y * y + x * x * y + 4

takeouchida

fn main() {
  let v: Result<Vec<i32>, _> = "1 2 3".split(" ").map(|w| w.parse()).collect();
  println!("{:?}", v); // => Ok([1, 2, 3])
}

takeouchida

lemma "∃ x. x + 1 = 3" (is "∃ x. ?P x")
proof
  show "?P 2" by simp
qed

(*
lemma "∃ x y. x + y + 1 = 3" (is "∃ x y. ?P x y")
proof
(*
Failed to refine any pending goal 

takeouchida

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma cons_rcons T (x1 x2 : T) s : x1 :: rcons s x2 = rcons (x1 :: s) x2.
Proof. done. Qed.

takeouchida

link(0, 0, 2,  0,  0, 2).  link(0, 1, 3,  0,  0, 3).  link(0, 2, 1, -1, -1, 4).  link(0, 3, 3,  0, -1, 0).  link(0, 4, 1,  0,  0, 1).
link(1, 0, 2,  0,  0, 3).  link(1, 1, 0,  0,  0, 4).  link(1, 2, 2,  0, -1, 0).  link(1, 3, 3,  1,  0, 1).  link(1, 4, 0,  1,  1, 2).
link(2, 0, 1,  0,  1, 2).  link(2, 1, 3,  0,  0, 4).  link(2, 2, 0,  0,  0, 0).  link(2, 3, 1,  0,  0, 0).  link(2, 4, 3,  1,  1, 2).
link(3, 0, 0,  0,  1, 3).  link(3, 1, 1, -1,  0, 3).  link(3, 2, 2, -1, -1, 4).  link(3, 3, 0,  0,  0, 1).  link(3, 4, 2,  0,  0, 1).

move((C1, X1, Y1, D1), [], (C2, X2, Y2, D2)) :- link(C1, D1, C2, DX, DY, D2), X2 is X1 + DX, Y2 is Y1 + DY.
move((C, X, Y, D1), [cw|Cs], S) :- D2 is (D1 + 4) mod 5, move((C, X, Y, D2), Cs, S).
move((C, X, Y, D1), [ccw|Cs], S) :- D2 is (D1 + 1) mod 5, move((C, X, Y, D2), Cs, S).

next_command([fw|Cs], [], Cs).

takeouchida

Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
Require Import ZArith Recdef.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Inductive cell := C0 | C1 | C2 | C3.
Inductive dir := D0 | D1 | D2 | D3 | D4.

takeouchida

(add-to-list 'load-path "~/.emacs.d/el-get/el-get")

(unless (require 'el-get nil 'noerror)
  (with-current-buffer
      (url-retrieve-synchronously
       "https://raw.githubusercontent.com/dimitri/el-get/master/el-get-install.el")
    (goto-char (point-max))
    (eval-print-last-sexp)))

(add-to-list 'el-get-recipe-path "~/.emacs.d/el-get-user/recipes")

takeouchida

object SpecExample extends App {
  // Application code
  case class ResourceX(name: String)
  case class ResourceY(name: String)

  def createResourceX(name: String): ResourceX = { println(s"Creating $name"); ResourceX(name) }
  def createResourceY(name: String): ResourceY = { println(s"Creating $name"); ResourceY(name) }

  // Utility code for testing
  trait Closeable[R] {

takeouchida

package object typeclasses {
  trait Functor[F[_]] { self =>
    def fmap[A, B](fa: F[A])(f: A => B): F[B]
  }

  trait Applicative[F[_]] extends Functor[F] { self =>
    def pure[A](a: => A): F[A]
    def ap[A, B](fa: F[A])(f: F[A => B]): F[B]
  }

takeouchida

// See this for details.
// http://www.jooq.org/doc/latest/manual/code-generation/custom-data-type-bindings/

package postgrestypes.bindings;

import org.jooq.*;
import org.jooq.impl.DSL;

import java.sql.SQLException;
import java.sql.SQLFeatureNotSupportedException;