ikedaisuke

ぷるーふさみっと2015、ライトニングトーク、ラジオー（仮）の台本

みなさん、こんにちは、「発表者」です。 この番組ではリスナーの皆さんに「定理証明」の話題をお届けいたします。 たぶん、今回が最初で最後だと思います。

これから15分ほどの間、お付き合いくださいませ。

それではさっそくメールを読み上げていきたいと思います。 ラジオネーム「とあるHaskell golfer」さんから質問をいただきました。

ikedaisuke

Real world (functional) programming with dependent types!
---------------------------------------------------------
* we want to write a program with /dependent types/
  * shallow embedding vs. deep embedding
* we want to prove some properties of each part of the program
* we need reasoning about programs
  * especially, a program will run correctly
    * interactiton with I/O
    * mutable state
    * etc.

ikedaisuke

-- % idris simple-uniq.idr -o uniq
module Main

getContents : IO String
getContents = go ""
  where go : String -> IO String
        go s = do case !(feof stdin) of
                    True  => return s
                    False => do t <- fread stdin
                                go (s ++ t)

ikedaisuke

Emacs の git クライアント magit の個人的なまとめです。正確かどうかは保証しません。

こんな cheat sheet を参照するくらいなら magit の公式ドキュメント読んだほうがいいと思う。

Magit!

バージョン

git

ikedaisuke

;; How to use:
;; impatient-mode
;; M-x imp-set-user-filter
;; markdown-filter
;; see also https://github.com/skeeto/impatient-mode
(defun markdown-filter (buffer)
  "Render a markdown document on your browser in real time by impatient-mode and markdown-mode."
  (princ
   (with-temp-buffer
     (let ((tempname (buffer-name)))

ikedaisuke

Search lemma on the fly in ProofGeneral

A helm extension for Search command.

/disambiguation/

• in the text, helm means Emacs-helm
• not means the HELM library of mathematics.