Seeker's eye
Thursday, 11 January 2018
Agda のプログラミングの続き
結構順調に進んでいて、
assert 見たいなところに等式を書いて refl で証明!
みたいにできるんですが...
二分木に4個入れた所で沈黙
おい。直前に入れたものは取れるのだが、二つ前だとダメだな。
でも、refl でなければ普通に eval で値は返ってくるんですけどね。まあ、Agda にはAgdaの都合があるんでしょう。
昨日はもつ鍋でしたが、さすがにテンパってるM2は釣れないか。いや、来てくれた人も。
No comments:
Post a Comment
Newer Post
Older Post
Home
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment