{"action":"created","issue":{"url":"https://api.github.com/repos/acl2/acl2/issues/459","labels_url":"https://api.github.com/repos/acl2/acl2/issues/459/labels{/name}","comments_url":"https://api.github.com/repos/acl2/acl2/issues/459/comments","events_url":"https://api.github.com/repos/acl2/acl2/issues/459/events","html_url":"https://github.com/acl2/acl2/issues/459","id":95738494,"number":459,"title":":doc auto-bindings potential bug?","user":{"login":"pennyan","id":9921924,"avatar_url":"https://avatars.githubusercontent.com/u/9921924?v=3","gravatar_id":"","url":"https://api.github.com/users/pennyan","html_url":"https://github.com/pennyan","followers_url":"https://api.github.com/users/pennyan/followers","following_url":"https://api.github.com/users/pennyan/following{/other_user}","gists_url":"https://api.github.com/users/pennyan/gists{/gist_id}","starred_url":"https://api.github.com/users/pennyan/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/pennyan/subscriptions","organizations_url":"https://api.github.com/users/pennyan/orgs","repos_url":"https://api.github.com/users/pennyan/repos","events_url":"https://api.github.com/users/pennyan/events{/privacy}","received_events_url":"https://api.github.com/users/pennyan/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-07-17T20:32:24Z","updated_at":"2015-07-17T20:58:15Z","closed_at":null,"body":"In the example,\r\n(def-gl-thm foo\r\n  ...\r\n  :g-bindings (auto-bindings               ; expands to:\r\n               (:nat opcode 8)             ; g-number with indices 0-8\r\n               (:int multiplier 16)        ; g-number with indices 9-25\r\n               (:bool enable)              ; g-boolean with index 26\r\n               (:mix (:nat a-bus 128)      ; }  g-numbers whose indicies\r\n                     (:nat b-bus 128)      ; }  are interleaved, 27 to 414\r\n                     (:nat c-bus 128))     ; }\r\n               (:nat fixup-bits 4)         ; g-number with indices 415-420\r\n               ))\r\n\r\nCould it be that the ranges in the comments should really be:\r\n; g-number with indices 0 - 7\r\n; g-number with indices 8 - 23\r\n; ....\r\n?"},"comment":{"url":"https://api.github.com/repos/acl2/acl2/issues/comments/122414252","html_url":"https://github.com/acl2/acl2/issues/459#issuecomment-122414252","issue_url":"https://api.github.com/repos/acl2/acl2/issues/459","id":122414252,"user":{"login":"ragerdl","id":2245886,"avatar_url":"https://avatars.githubusercontent.com/u/2245886?v=3","gravatar_id":"","url":"https://api.github.com/users/ragerdl","html_url":"https://github.com/ragerdl","followers_url":"https://api.github.com/users/ragerdl/followers","following_url":"https://api.github.com/users/ragerdl/following{/other_user}","gists_url":"https://api.github.com/users/ragerdl/gists{/gist_id}","starred_url":"https://api.github.com/users/ragerdl/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ragerdl/subscriptions","organizations_url":"https://api.github.com/users/ragerdl/orgs","repos_url":"https://api.github.com/users/ragerdl/repos","events_url":"https://api.github.com/users/ragerdl/events{/privacy}","received_events_url":"https://api.github.com/users/ragerdl/received_events","type":"User","site_admin":false},"created_at":"2015-07-17T20:58:15Z","updated_at":"2015-07-17T20:58:15Z","body":"Indeed, at least the first couple are correct so I'll go ahead and close this."}}