潜水をしているような気分だ。

diary

潜水をしているような気分だ。深いところで何かを探っていて、ふっと海面から顔を出し、息をする。そしてまた深いところに潜り直す。

こういう気分になったのは修士課程以来だ。

何を探しているのかはわからないし、これがいい傾向なのかすらわからない。

pc

パソコンの調子が何かおかしい。

おそらくこいつが悪さをしている。

雑に交換しよう。

今日の勉強

team

メモを一通り作れたので、summaryとして箇条書きを1つのファイルにまとめ、セクションを適当に区切った。

rust

TRPL pp.146-155

ベクタの中身を読む方法:

  1. ベクタがある。
  2. ベクタのすでにある要素への参照を取る。
    1. 不変借用が発生する。
  3. ベクタにpushする。
    1. 可変借用が発生する。
    2. ここで可変借用が発生するのは、ベクタが現在存在する位置に隣あっている要素を入れるだけの領域がない場合に、メモリの新規確保をして、古い要素を新しいスペースにコピーする、というベクタの動作法がある。
  4. step2の参照を使おうとするとCompile Errorが発生する。

文字列

文字列に添え字でアクセスする

isabelle

Concrete Semantics

証明を追いかけたもの

疑問:declareの役割

declare assign_simp[simp]という表現がないと証明できない箇所があった。

declareの役割は何か? useみたいな感じで引っ張ってきて、それにsimpで使うように宣言したりするようにすることか?

その線でやったら、declareしなくてもできたからこの認識で多少あっていそうだ。

team  log  pc  rust  isabelle