# HG changeset patch
# User autobackup
# Date 1619190604 -32400
# Node ID afba7141d1a6d2b5fa958ae5be48e533b4ca7efc
# Parent  34cd1ff59d3409b5224e1be3525ba03681616e48
backup 2021-04-24

diff -r 34cd1ff59d34 -r afba7141d1a6 user/soto/log/2021-04-20.md
--- a/user/soto/log/2021-04-20.md	Wed Apr 21 00:10:03 2021 +0900
+++ b/user/soto/log/2021-04-20.md	Sat Apr 24 00:10:04 2021 +0900
@@ -17,12 +17,6 @@
 
 - agdaが変数への再代入を許していない為、ループが存在し、かつ再代入がプログラムに含まれるデータ構造である赤黒木の検証を行う
 
-# 研究目的(修士の方)(途中)
-- CbCにはあまりよくない部分がある
-    - interfaceとか
-
-- RustをContinuetion styleにしたものを作成し、Agdaで検証する
-
 # やった事
 
 - モデル検査について調べていた
@@ -30,6 +24,11 @@
 - LLVMについても勉強したかった
     - 「きつねさんでもわかるLLVM」を読んでいたが、難しくて寝てしまった(つまり僕の理解力はきつねさん以下だった…)
 
+- Gears Agdaで Red Black Tree を作成する
+    - 卒論時に作成していたものを修正するなどしていた
+        - deleteの部分に実は上手くできていない所があったのでリファクタリングをしています…
+    - 実はもうちょっとでできそうな感じがある。
+
 ## モデル検査について
 Agdaでモデル検査をする事をkono先生が言っていたので、調べていた
 
@@ -51,11 +50,11 @@
 ## 今後やりたい事/やらないといけない事
 - RustはLLVMで出来ている
     - ので、LLVM側に Continuation Style を適応出来たら嬉しい
-- Agdaで Red Black Tree を作成する
-    - 実はもうちょっとでできそうな感じがある。頑張ってみる
+
 - 研究計画書
     - なぜかアナウンスがまるでない…
 
 # 余談
 - M1 MacBook Air でAgda on Spacemacs が動くか検証していた
-    - ちゃんと動きました。やったね
\ No newline at end of file
+    - ちゃんと動きました。
+    - 過去にemacs plusでAgdaが動くのは確認していた
\ No newline at end of file