{"action":"created","issue":{"url":"https://api.github.com/repos/acl2/acl2/issues/539","labels_url":"https://api.github.com/repos/acl2/acl2/issues/539/labels{/name}","comments_url":"https://api.github.com/repos/acl2/acl2/issues/539/comments","events_url":"https://api.github.com/repos/acl2/acl2/issues/539/events","html_url":"https://github.com/acl2/acl2/issues/539","id":115407379,"number":539,"title":"std::define more-returns and GL","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},"labels":[{"url":"https://api.github.com/repos/acl2/acl2/labels/Component:%20GL","name":"Component: GL","color":"FFFFFF"},{"url":"https://api.github.com/repos/acl2/acl2/labels/Component:%20Std","name":"Component: Std","color":"009800"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2015-11-06T00:27:50Z","updated_at":"2015-11-06T01:15:28Z","closed_at":null,"body":"It'd be nice if std::define's more-returns syntax could be modified to accommodate the use of GL to prove return types.  Even just having keywords to specify the hyps and binding, similar to the SVex recomposition proof setup would be nice."},"comment":{"url":"https://api.github.com/repos/acl2/acl2/issues/comments/154253053","html_url":"https://github.com/acl2/acl2/issues/539#issuecomment-154253053","issue_url":"https://api.github.com/repos/acl2/acl2/issues/539","id":154253053,"user":{"login":"jaredcdavis","id":6493363,"avatar_url":"https://avatars.githubusercontent.com/u/6493363?v=3","gravatar_id":"","url":"https://api.github.com/users/jaredcdavis","html_url":"https://github.com/jaredcdavis","followers_url":"https://api.github.com/users/jaredcdavis/followers","following_url":"https://api.github.com/users/jaredcdavis/following{/other_user}","gists_url":"https://api.github.com/users/jaredcdavis/gists{/gist_id}","starred_url":"https://api.github.com/users/jaredcdavis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jaredcdavis/subscriptions","organizations_url":"https://api.github.com/users/jaredcdavis/orgs","repos_url":"https://api.github.com/users/jaredcdavis/repos","events_url":"https://api.github.com/users/jaredcdavis/events{/privacy}","received_events_url":"https://api.github.com/users/jaredcdavis/received_events","type":"User","site_admin":false},"created_at":"2015-11-06T01:15:28Z","updated_at":"2015-11-06T01:15:28Z","body":"Offhand it seems pretty messy (just dependency-wise) to try to modify `more-returns` itself to know about gl.  That said, it would probably be pretty straightforward to write a custom `more-returns-gl` macro that provided support for `g-bindings` and so forth but was otherwise styled after `more-returns`, and used its same mechanisms to know which which function is being defined, the names of the return values, etc.  This would probably be a fine addition to GL, if someone wants to write it."}}