pasberth

Theorem syllogism : forall (A B C : Prop), (B -> C) -> (A -> B) -> A -> C.
Proof.
  intros A B C H H0 H1.
  apply H.
  apply H0.
  apply H1.
Qed.

pasberth

{-# LANGUAGE OverloadedStrings #-}
module Main where

import Data.ByteString

default (ByteString)

s = "hello world"
-- :: ByteString
-- デフォルトが ByteSTring になる

pasberth

#include <string>
#include <vector>
#include <list>
#include <iostream>

template<class Iterator>
void print_all(Iterator first, Iterator last)
{
  while (first != last)
  {

pasberth

#include <iostream>

typedef void (*f_t)();

class Base {
public:
  virtual void f();
};

struct Derivied : public Base {

pasberth

import Data.IORef

doWhile :: Monad m => m Bool -> m a -> m a
doWhile test body = do
  x <- body
  testResult <- test
  if testResult
    then doWhile test body
    else return x

pasberth

Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q.
Proof.
  intro P.
  intro Q.
  intro H.
  apply H.
Qed.

pasberth

import qualified System.Environment     as E
import qualified Data.HashMap.Strict    as M

mathematicalScriptMap :: M.HashMap Char Char
mathematicalScriptMap = M.fromList [
    ('A', '\x1D49C'),
    ('B', '\x0212C'),
    ('C', '\x1D49E'),
    ('D', '\x1D49F'),
    ('E', '\x02130'),

pasberth

# -*- coding: utf-8 -*-

s = gets.chomp

if s == "true" || s == "真" then
  puts "OK"
else
  puts "NG"
end

pasberth

def random
  [true, false].sample
end

if random then
  puts "OK"
else
  puts "NG"
end

pasberth

--ちんちんっぽいことするやつ
import System.Random
chimpo :: String -> IO String
randomString :: String -> IO String

chimpo c = do s <- randomString c
              if take 4 c == "ABCDE"
		 then return $ c ++ ("なんか終わりました" ++ (show (length c )))
		 else chimpo s