MiyamonY

OMake Tips

ビルドするソースファイルの指定

• 拡張子でファイルを指定する場合、以下のように指定できる。 \$(removesuffix $(filter %.ml, $(ls .)))\

MiyamonY

nose(Python unittestフレームワーク) tips

nose

• `nosetests` コマンドでカレントディレクトリ以下のテストファイル中のテストを実 行する。

MiyamonY

Theorem instantiated :
forall m:nat,
  m <= 0 -> m = 0.
Proof.
  intros. induction H.
  - reflexivity.
  - subst. Abort.

Theorem generalized :
  forall m n,

MiyamonY

Definition Plus: nat -> nat -> nat.
  intros x.
  elim x using nat_rec.
  - intros y. apply y.
  - intros x' plus_x' y. apply (S (plus_x' y)).
Defined.

Print Plus.
(* Plus =  *)
(* fun x : nat => *)

MiyamonY

Require Import Fin.
Print Module Fin.

(** Finはfinite setの略で、Fin.t n でサイズnの有限の集合を表わす型。 *)

Print Fin.t.
(* Inductive t : nat -> Set := *)
(*     F1 : forall n : nat, t (S n) | FS : forall n : nat, t n -> t (S n) *)

Check F1: Fin.t 3.              (* 0 *)

MiyamonY

# coding: utf-8

# In[26]:

import numpy as np
import matplotlib.pyplot as plt
import matplotlib.dates as mdates
from datetime import datetime
from __future__ import print_function

MiyamonY

import Data.List
import Data.Char
import qualified Data.Map as Map

-- head' :: [a] -> a
-- head' [] = error "Can't call head on an emply list, dummy!"
-- head' (x : _) = x

tell :: (Show a) => [a] -> String
tell [] = "The list is empty"

MiyamonY

module Geometry
       ( sphereVolume,
         sphereArea,
         cubeVolume,
         cubeArea,
         cuboidArea,
         cuboidVolume) where

sphereVolume :: Float -> Float
sphereVolume radius = (4.0 / 3.0) * pi * (radius ^ 3)

MiyamonY

module Shapes
       ( Point (..),
         Shape (..),
         area,
         nudge,
         baseCircle,
         baseRect ) where

-- data Bool = False | True

MiyamonY

import qualified Data.Map as Map
-- record
-- data Person = Person {firstName :: String,
--                       lastName :: String,
--                       age :: Int,
--                       height :: Float,
--                       phoneNumber :: String,
--                       flavor :: String} deriving(Show)
-- guy = Person "Buddy" "Finklestein" 43 184.2 "562-2928" "Chocolate"