Public
- Public
- Network
- Groups
- Popular
- People

Conversation

Notices

きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 08-Nov-2020 00:44:07 JST きゅーけー

順序数難しいACL2 以外で実装している例ないのかな

In conversation Sunday, 08-Nov-2020 00:44:07 JST from mastodon.tojo.tokyo permalink
- きゅーけー (tojoqk@mastodon.tojo.tokyo)'s status on Sunday, 08-Nov-2020 00:58:33 JST きゅーけー
  in reply to
  
  ちゃんと o-p の実装を見てやっと納得した。+ の右側には必ず最初の指数部よりも小さなやつしかでてこないように定義されているから安心していいのか。順序数とか難しすぎるので ACL2 の実装を Scheme に翻訳して使おう……。https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/ACL2____O-P?path=3574/6842/3819/225/243
  
  In conversation Sunday, 08-Nov-2020 00:58:33 JST permalink

Feeds