kencoba

(* 新妻弘，「演習　群・環・体　入門」，共立出版株式会社 より *)
Require Import ZArith.
Open Scope Z_scope.

Theorem thm_1_1 : forall a b c : Z , a + b = a + c -> b = c.
Proof.
  intros a b c H.
  apply Z.add_cancel_l with (p := a).
  assumption.
Qed.

kencoba

import java.io.IOException;
import java.io.PrintWriter;

import javax.servlet.ServletException;
import javax.servlet.annotation.WebServlet;
import javax.servlet.http.HttpServlet;
import javax.servlet.http.HttpServletRequest;
import javax.servlet.http.HttpServletResponse;
import javax.servlet.http.HttpSession;

kencoba

// http://en.wikipedia.org/wiki/Decorator_pattern

trait Coffee {
  def cost:Double
  def ingredients: String
}

class SimpleCoffee extends Coffee {
  override def cost = 1
  override def ingredients = "Coffee"

kencoba

Inductive day : Type :=
  | monday : day
  | tuesday : day
  | wednesday : day
  | thursday : day
  | friday : day
  | saturday : day
  | sunday : day.

Definition next_weekday (d:day) : day :=

kencoba

abstract class Product

abstract class PizzaBuilder {
  var dough: String
  var sauce: String
  var topping: String

  def withDough(dough: String): PizzaBuilder
  def withSauce(sauce: String): PizzaBuilder
  def withTopping(topping: String): PizzaBuilder

kencoba

class Request
end

class Read < Request
  attr_reader :var

  def initialize(var)
    @var = var
  end

kencoba

class Request:
    pass


class Read(Request):
    def __init__(self, var):
        self.var = var


class Write(Request):

kencoba

fn main() {
    println!("{n}P{r} = {x}", n = 5, r = 2, x = permutation(5, 2));
    println!("{n}C{r} = {x}", n = 5, r = 2, x = combination(5, 2));
}

pub fn permutation(n: i64, r: i64) -> i64 {
    let mut result = 1;
    for i in (n - r + 1)..=n {
        result *= i;
    }

kencoba

use std::collections::HashMap;

struct Checker {
    memo: HashMap<(i64, i64), i64>,
    max_seat_at_one_table: i64,
}

impl Checker {
    pub fn check(&mut self, remain: i64, pre: i64) -> i64 {
        match &self.memo.get(&(remain, pre)) {

kencoba

Sub PPCode()

    ActiveDocument.Select

    Dim codelines As Paragraphs
    Set codelines = Selection.Paragraphs

    Selection.Copy

    Dim lines As Long