記事一覧
Coq 演習 3
http://herb.h.kobe-u.ac.jp/coq/coq.pdf の続き。 2.2.5 まで読んだ。 演習問題 3. Section PredicateLogic.Variable A: Type.Variable P Q: A -> Prop.Variable R: A -…
Coq 演習 2
http://herb.h.kobe-u.ac.jp/coq/coq.pdf の続き。 2.1.9 古典論理 まで読んだ。排中律を手に入れた。 演習問題 2. Require Import Classical.Variable A B C: Prop.Lemm…
Coq 演習 1
こちらの PDF が素晴らしいとのことなので 「Coq/SSReflect/MathComp による定理証明」より先にやってみる。 http://herb.h.kobe-u.ac.jp/coq/coq.pdf 2.1.8 まで読んだの…
実例によるPureScript 8 章 - 2
Eff モナドに関するところ。説明と演習では Eff が使われているが、Eff は deprecated になっており、Effect を使う必要がある。ST も変わっている。以下の記事が参考になった。
safeDivide2 :: Int -> Int -> Effect IntsafeDivide2 _ 0 = throwException $ error $ "Divided by 0"s
実例によるPureScript 8 章 - 1
モナドが登場した。課題がムズくて時間がかかりそうなので分割することにする。
thirdElement :: forall a. Array a -> Maybe athirdElement xs = do a <- tail xs b <- tail a c <- head b pure c
難しい。期待する答えを返していると思うが、自分の書いたコードを見てもまだよく理解できていない。
実例によるPureScript 7 章
Applicative の章。難易度が上がって来ている気がする。演習はなんとかこなせたが、正直まだ全然適切に利用できる気がしない。慣れるものなんだろうか。
main :: Effect Unitmain = do logShow $ lift2 (+) (Just 2) (Just 3) logShow $ lift2 (+) (Just 2) Nothing logShow $ lift
実例によるPureScript 6 章
型クラスの章。型クラスとそのインスタンスの関係は、普通のオブジェクト志向言語のクラスとインスタンスが一個上にずれている感じ。
これは book に答えがあるが。
instance shapeShow :: Show Shape where show shape = showShape shape
instance showComplex :: Show Complex where sho
実例によるPureScript 5 章
パターン照合の章である。使いこなせれば強力なのは理解できる。記法が慣れないのは書いて覚えるしかないか。
factorial :: Int -> Intfactorial 0 = 1factorial n = n * factorial (n - 1)
pascalsRule :: Int -> Int -> IntpascalsRule 0 _ = 1pascalsRule _ 0 = 1pa
実例によるPureScript 4 章
演習はいっぱいあった。A, B, C, D, E とする。
演習 A.
こんなのでいいのかな。
isEven :: Int -> BooleanisEven n = if n == 0 then true else if n == 1 then false else if n < 0 then isEven (n + 2) else
Coq 演習 3
http://herb.h.kobe-u.ac.jp/coq/coq.pdf の続き。
2.2.5 まで読んだ。
演習問題 3.
Section PredicateLogic.Variable A: Type.Variable P Q: A -> Prop.Variable R: A -> (A -> Prop).Variable t: A.Lemma all_imply: (forall x
Coq 演習 2
http://herb.h.kobe-u.ac.jp/coq/coq.pdf の続き。
2.1.9 古典論理 まで読んだ。排中律を手に入れた。
演習問題 2.
Require Import Classical.Variable A B C: Prop.Lemma Taiguu: (~B -> ~A) -> (A -> B).Proof.intros.apply NNPP.intro.gener
実例による PureScript 3 章
build の前にいくつかの module のインストールが必要だった。
$ spago install purescript-controｌ$ spago install purescript-maybe$ spago install purescript-lists$ spago build$ spago repl> import Data.AddressBook > address = {
Coq 演習 1
こちらの PDF が素晴らしいとのことなので 「Coq/SSReflect/MathComp による定理証明」より先にやってみる。
http://herb.h.kobe-u.ac.jp/coq/coq.pdf
2.1.8 まで読んだので演習問題をやる。2.1.5 の論理和のところでちょっと詰まった。destruct して 2 つにゴールが割れるところは、1 つ目と 2 つ目でゴールペインの仮定が
実例による PureScript 2 章
ついでに PureScript の勉強も始める。
以下をやり遂げることをまずは最初の目標とする。序文に、最新の状態と異なる、と書いてあるのでメモがてら差分を残していきたい。
Chapter 2.
まず Math がない。purescript-numbers に変わったらしい。spago が良いようなので初期化も spago に乗り換える。
$ spago init$ spago instal